proposition: Lemma open_subspaceP (U : set T) : open (U : set (subspace A)) <-> exists V, open (V : set T) /\ V `&` A = U `&` A.
proof: Proof. split; first last. case=> V [oV UV]; rewrite -open_subspaceIT -UV. move=> x //= []; case: nbhs_subspaceP; rewrite //= withinE. move=> ? ? _; exists V; last by rewrite -setIA setIid. by move: oV; rewrite openE /interior; apply. rewrite -open_subspaceIT => oUA. have oxF : (forall (x : T), (U `&` A) x -> exists V, (open_nbhs (x : T) V) /\ (V `&` A `<=` U `&` A)). move=> x /[dup] UAx /= [??]; move: (oUA _ UAx); case: nbhs_subspaceP => // ?. rewrite withinE /= => [[V nbhsV UV]]; rewrite -setIA setIid in UV. exists V^°; split; first rewrite open_nbhsE; first split => //. - exact: open_interior. - exact: nbhs_interior. - by rewrite UV=> t [/interior_subset] ??; split. pose f (x : T) := if pselect ((U `&` A) x) is left e then projT1 (cid (oxF x e)) else set0. set V := \bigcup_(x in (U `&` A)) (f x); exists V; split. apply: bigcup_open => i UAi; rewrite /f; case: pselect => // ?; case: (cid _). by move=> //= W; rewrite open_nbhsE=> -[[]]. rewrite eqEsubset /V /f; split. move=> t [[u]] UAu /=; case: pselect => //= ?. by case: (cid _) => //= W [] _ + ? ?; apply; split. move=> t UAt; split => //; last by case: UAt. exists t => //; case: pselect => //= [[? ?]]. by case: (cid _) => //= W [] [] _. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed