proposition: Lemma isOpen_hfalse : isOpen (λ _ : T, hfalse).
proof: Proof. apply isSetOfOpen_hfalse. intros P H. now apply isOpen_union. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Topology.Filters UniMath.Algebra.Groups UniMath.Algebra.DivisionRig UniMath.Algebra.ConstructiveStructures