proposition: Lemma topological_property_compact : topological_property compact.
proof: Proof. intros X Y f [g Hcont_f Hcont_g Hgf Hfg] Hcomp F H eq. destruct (Hcomp (inverse_image (inverse_image g) F)) as [F' [H1 [H2 H3]]]. - intros. rewrite <- (inverse_image_id_comp Hgf). apply Hcont_f, H. now destruct H0. - erewrite <- inverse_image_full, <- (inverse_image_id_comp Hgf (FamilyUnion _)). f_equal. now rewrite <- (inverse_image_family_union F Hgf), inverse_image_id_comp. - exists (inverse_image (inverse_image f) F'). split; [|split]. + apply injective_finite_inverse_image; auto. apply inverse_image_surjective_injective. apply invertible_impl_bijective. exists g; assumption. + intros S [Hin]. destruct (H2 _ Hin) as [H0]. now rewrite inverse_image_id_comp in H0. + rewrite <- (inverse_image_family_union _ Hfg Hgf), H3. apply inverse_image_full. Qed.
imports: Coq(ClassicalChoice Program.Subset) ZornsLemma(Finite_sets Powerset_facts) Topology(FiltersAndNets)