proposition: Lemma neighborhood_isOpen (P : T → hProp) : (∏ x, P x → neighborhood x P) <-> isOpen P.
proof: Proof. split. - intros Hp. assert (H : ∏ A : T → hProp, isaprop (∏ y : T, A y → P y)). { intros A. apply impred_isaprop. intro y. apply isapropimpl. apply propproperty. } set (Q := λ A : T → hProp, isOpen A ∧ (make_hProp (∏ y : T, A y → P y) (H A))). assert (X : P = (union Q)). { apply funextfun. intros x. apply hPropUnivalence. - intros Px. generalize (Hp _ Px). apply hinhfun. intros A. exists (pr1 A) ; split. + split. * apply (pr2 (pr1 A)). * exact (pr2 (pr2 A)). + exact (pr1 (pr2 A)). - apply hinhuniv. intros A. apply (pr2 (pr1 (pr2 A))). exact (pr2 (pr2 A)). } rewrite X. apply isOpen_union. intros A Ha. apply (pr1 Ha). - intros Hp x Px. apply hinhpr. exists (P,,Hp). split. + exact Px. + intros y Py. exact Py. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Topology.Filters UniMath.Algebra.Groups UniMath.Algebra.DivisionRig UniMath.Algebra.ConstructiveStructures