proposition: Lemma TopologyGenerated_included {X : hSet} : ∏ (O : (X → hProp) → hProp) (P : X → hProp), O P → isOpen (T := TopologyGenerated O) P.
proof: Proof. intros O P Op. apply neighborhood_isOpen. intros x Hx. apply TopologyFromNeighborhood_correct. apply hinhpr. exists (singletonSequence P). repeat split. - induction n as [n Hn]. exact Op. - intros n ; induction n as [n Hn]. exact Hx. - intros y Hy. now apply (Hy (0%nat,,paths_refl _)). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Topology.Filters UniMath.Algebra.Groups UniMath.Algebra.DivisionRig UniMath.Algebra.ConstructiveStructures