fact: Definition isSetOfOpen_finite_intersection := ∏ (P : Sequence (X → hProp)), (∏ m, O (P m)) → O (finite_intersection P).
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Topology.Filters UniMath.Algebra.Groups UniMath.Algebra.DivisionRig UniMath.Algebra.ConstructiveStructures