proposition: Lemma withinU_continuous {U} A B (f : T -> U) : closed A -> closed B -> {within A, continuous f} -> {within B, continuous f} -> {within A `|` B, continuous f}.
proof: Proof. move=> ? ? ctsA ctsB; apply/continuous_closedP => W oW. case/continuous_closedP/(_ _ oW)/closed_subspaceP: ctsA => V1 [? V1W]. case/continuous_closedP/(_ _ oW)/closed_subspaceP: ctsB => V2 [? V2W]. apply/closed_subspaceP; exists ((V1 `&` A) `|` (V2 `&` B)); split. by apply: closedU; exact: closedI. rewrite [RHS]setIUr -V2W -V1W eqEsubset; split=> ?. by case=> [[][]] ? ? [] ?; [left | left | right | right]; split. by case=> [][] ? ?; split=> []; [left; split | left | right; split | right]. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed