proposition: Lemma nbhsNKe (R : realFieldType) (z : \bar R) (A : set (\bar R)) : nbhs (- z) (-%E @` A) -> nbhs z A.
proof: Proof. rewrite nbhsNe => -[S zS] SA; rewrite -(oppeK z) nbhsNe. exists (-%E @` S); first by rewrite nbhsNe; exists S. rewrite predeqE => x; split => [[y [u Su <-{y} <-]]|Ax]. rewrite oppeK. move: SA; rewrite predeqE => /(_ (- u)) [h _]. have : (exists2 y, S y & - y = - u) by exists u. by move/h => -[y Ay] /eqP; rewrite eqe_opp => /eqP <-. exists (- x); last by rewrite oppeK. exists x => //. move: SA; rewrite predeqE => /(_ (- x)) [_ h]. have : (-%E @` A) (- x) by exists x. by move/h => [y Sy] /eqP; rewrite eqe_opp => /eqP <-. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(fsbigop cardinality set_interval) reals signed topology constructive_ereal