proposition: Lemma base_default_1 : ∏ P : T → hProp, base_default P → neighborhood x P.
proof: Proof. intros P Hp. apply hinhpr. exists (P,,(pr1 Hp)) ; split. - exact (pr2 Hp). - intros. assumption. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Topology.Filters UniMath.Algebra.Groups UniMath.Algebra.DivisionRig UniMath.Algebra.ConstructiveStructures