proposition: Lemma isNeighborhood_isPreFilter {X : hSet} N : isNeighborhood N -> ∏ x : X, isPreFilter (N x).
proof: Proof. intros Hn x. split. - apply (pr1 Hn). - apply isfilter_finite_intersection_carac. + apply (pr1 (pr2 Hn)). + apply (pr1 (pr2 (pr2 Hn))). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Topology.Filters UniMath.Algebra.Groups UniMath.Algebra.DivisionRig UniMath.Algebra.ConstructiveStructures