proposition: Lemma topologygenerated_neighborhood : ∏ (x : X) (P : X → hProp), topologygenerated x P → ∃ Q : X → hProp, topologygenerated x Q × (∏ y : X, Q y → topologygenerated y P).
proof: Proof. intros x P. apply hinhfun. intros L. exists (finite_intersection (pr1 L)). split. - apply hinhpr. exists (pr1 L). repeat split. + exact (pr1 (pr2 L)). + exact (pr1 (pr2 (pr2 L))). + intros. assumption. - intros y Hy. apply hinhpr. exists (pr1 L). repeat split. + exact (pr1 (pr2 L)). + exact Hy. + exact (pr2 (pr2 (pr2 L))). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Topology.Filters UniMath.Algebra.Groups UniMath.Algebra.DivisionRig UniMath.Algebra.ConstructiveStructures