proposition: Lemma continuous_pr2 {U V : TopologicalSpace} : continuous (U := TopologyDirprod U V) (λ (xy : U × V), pr2 xy).
proof: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Topology.Filters UniMath.Algebra.Groups UniMath.Algebra.DivisionRig UniMath.Algebra.ConstructiveStructures