Lemma topologydirprod_imply : ∏ x : U × V, isfilter_imply (topologydirprod x). Proof. intros x A B H. apply hinhfun. intros AB. exists (pr1 AB), (pr1 (pr2 AB)) ; split ; [ | split]. - exact (pr1 (pr2 (pr2 AB))). - exact (pr1 (pr2 (pr2 (pr2 AB)))). - intros x' y' Hx' Hy'. now apply H, (pr2 (pr2 (pr2 (pr2 AB)))). 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 _ _).