Lemma continuous_pr2 {U V : TopologicalSpace} : continuous (U := TopologyDirprod U V) (λ (xy : U × V), pr2 xy). Proof. intros xy P. apply hinhuniv. intros O. simple refine (filter_imply _ _ _ _ _). - exact (pr1 (pr1 O)). - exact (pr2 (pr2 O)). - apply hinhpr. use tpair. + use tpair. * apply (λ xy : U × V, pr1 O (pr2 xy)). * intros xy' Oxy. apply hinhpr. exists (λ _, htrue), (pr1 O). repeat split. ** exact isOpen_htrue. ** exact Oxy. ** exact (pr2 (pr1 O)). ** intros. assumption. + repeat split. * exact (pr1 (pr2 O)). * intros. assumption. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Groups. Require Import UniMath.Algebra.DivisionRig. Require Import UniMath.Algebra.ConstructiveStructures. Section TopologyFromNeighborhood. End TopologyFromNeighborhood. Definition TopologyFromNeighborhood {X : hSet} Lemma TopologyFromNeighborhood_correct {X : hSet} N x P <-> neighborhood (T := TopologyFromNeighborhood N H) x P. simple refine (TopologyFromNeighborhood _ _). apply TopologyFromNeighborhood_correct. simple refine (TopologyFromNeighborhood _ _). apply TopologyFromNeighborhood_correct. simple refine (TopologyFromNeighborhood _ _).