proposition: Lemma locally2d_correct {T S : TopologicalSpace} (x : T) (y : S) : ∏ P : T × S → hProp, locally2d x y P <-> locally (T := TopologyDirprod T S) (x,,y) P.
proof: Proof. intros P. split ; apply hinhuniv. - intros A. apply TopologyFromNeighborhood_correct. generalize (pr1 (pr2 (pr2 A))) (pr1 (pr2 (pr2 (pr2 A)))). apply hinhfun2. intros Ox Oy. exists (pr1 Ox), (pr1 Oy). repeat split. + exact (pr1 (pr2 Ox)). + exact (pr2 (pr1 Ox)). + exact (pr1 (pr2 Oy)). + exact (pr2 (pr1 Oy)). + intros x' y' Hx' Hy'. apply (pr2 (pr2 (pr2 (pr2 A)))). * now apply (pr2 (pr2 Ox)). * now apply (pr2 (pr2 Oy)). - intros O. generalize (pr2 (pr1 O) _ (pr1 (pr2 O))). apply hinhfun. intros A. exists (pr1 A), (pr1 (pr2 A)). repeat split. + apply (pr2 (neighborhood_isOpen _)). * exact (pr2 (pr1 (pr2 (pr2 A)))). * exact (pr1 (pr1 (pr2 (pr2 A)))). + apply (pr2 (neighborhood_isOpen _)). * exact (pr2 (pr1 (pr2 (pr2 (pr2 A))))). * exact (pr1 (pr1 (pr2 (pr2 (pr2 A))))). + intros x' y' Ax' Ay'. apply (pr2 (pr2 O)). now apply (pr2 (pr2 (pr2 (pr2 A)))). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Topology.Filters UniMath.Algebra.Groups UniMath.Algebra.DivisionRig UniMath.Algebra.ConstructiveStructures