proposition: Lemma isNeighborhood_neighborhood {T : TopologicalSpace} : isNeighborhood (neighborhood (T := T)).
proof: Proof. repeat split. - intros x A B. apply (neighborhood_imply x). - intros x. apply (pr2 (neighborhood_isOpen _)). + exact (isOpen_htrue (T := T)). + apply tt. - intros A B. apply neighborhood_and. - intros x P. apply neighborhood_point. - intros x P. apply neighborhood_neighborhood. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Topology.Filters UniMath.Algebra.Groups UniMath.Algebra.DivisionRig UniMath.Algebra.ConstructiveStructures