proposition: Lemma neighborhood_equiv {T : TopologicalSpace} (x : T) (B : base_of_neighborhood x) : ∏ P, neighborhood' x B P <-> neighborhood x P.
proof: Proof. split. - apply hinhuniv. intros O. generalize ((pr1 (pr2 B)) (pr1 O) (pr1 (pr2 O))). apply neighborhood_imply. exact (pr2 (pr2 O)). - intros Hp. generalize (pr2 (pr2 B) P Hp). apply hinhfun. intros O. exists (pr1 O). exact (pr2 O). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Topology.Filters UniMath.Algebra.Groups UniMath.Algebra.DivisionRig UniMath.Algebra.ConstructiveStructures