proposition: Lemma base_default_2 : ∏ P : T → hProp, neighborhood x P → ∃ Q : T → hProp, base_default Q × (∏ t : T, Q t → P t).
proof: Proof. intros P. apply hinhfun. intros Q. exists (pr1 Q). repeat split. - exact (pr2 (pr1 Q)). - exact (pr1 (pr2 Q)). - exact (pr2 (pr2 Q)). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Topology.Filters UniMath.Algebra.Groups UniMath.Algebra.DivisionRig UniMath.Algebra.ConstructiveStructures