proposition: Lemma closedN (R : numFieldType) (A : set R) : closed A -> closed [set - x | x in A].
proof: Proof. move=> Acl x clNAx. suff /Acl : closure A (- x) by exists (- x)=> //; rewrite opprK. move=> B oppx_B; have : [set - x | x in A] `&` [set - x | x in B] !=set0. by apply: clNAx; rewrite -[x]opprK nbhsNimage; exists B. move=> [y [[z Az oppzey] [t Bt opptey]]]; exists (- y). by split; [rewrite -oppzey opprK|rewrite -opptey opprK]. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrint ssrnum finmap matrix) mathcomp(rat interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality set_interval Rstruct) ereal reals signed topology prodnormedzmodule