fact: Definition is_base_of_neighborhood {T : TopologicalSpace} (x : T) (B : (T → hProp) → hProp) := (∏ P : T → hProp, B P → neighborhood x P) × (∏ P : T → hProp, neighborhood x P → ∃ Q : T → hProp, B Q × (∏ t : T, Q t → P t)).
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Topology.Filters UniMath.Algebra.Groups UniMath.Algebra.DivisionRig UniMath.Algebra.ConstructiveStructures