proposition: Lemma compact_subspaceIP (U : set T) : compact (U `&` A : set (subspace A)) <-> compact (U `&` A : set T).
proof: Proof. rewrite ?compact_ultra /=. split=> + F UF FUA => /(_ F UF FUA) [x] [[Ux Ax] Fp]. exists x; split=> //; move/subspace_cvgP: Fp => /(_ Ax) Fx. by apply: cvg_trans; [exact: Fx | exact: cvg_within]. exists x; split=> //; apply/subspace_cvgP => //. rewrite withinE => W/= -[V nbhsV WV]; apply: filterS (V `&` (U `&` A)) _ _ _. by rewrite setIC -setIA [A `&` _]setIC -WV=>?[]?[]. by apply: filterI; rewrite nbhs_simpl //; exact: Fp. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed