proposition: Lemma zariski_topology_union : isSetOfOpen_union zariski_topology.
proof: Proof. intros O H0. unfold zariski_topology. set (S := λ A, ∃ U, O U ∧ U ≡ (λ p, A ⊈ p)). apply hinhpr. exists (union S). intro p. apply issymm_logeq, (logeq_trans (union_not_contained_in S p)). unfold union. use make_dirprod; intro H. - use (hinhuniv _ H); intro HA. induction HA as [A HA]. use (hinhfun _ (dirprod_pr1 HA)); intro HU. induction HU as [U HU]. exists U. use make_dirprod. + exact (dirprod_pr1 HU). + apply (dirprod_pr2 (dirprod_pr2 HU p)), (dirprod_pr2 HA). - use (hinhuniv _ H); intro HU. induction HU as [U HU]. use (hinhfun _ (H0 U (dirprod_pr1 HU))); intro HA. induction HA as [A HA]. exists A. use make_dirprod. + apply hinhpr. exists U. exact (make_dirprod (dirprod_pr1 HU) HA). + apply (dirprod_pr1 (HA p)), (dirprod_pr2 HU). Defined.
imports: UniMath.Algebra.RigsAndRings UniMath.Algebra.RigsAndRings.Ideals UniMath.MoreFoundations.AxiomOfChoice UniMath.MoreFoundations.Subtypes UniMath.Topology.Topology UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.Categories.Commring UniMath.AlgebraicGeometry.Topology UniMath.AlgebraicGeometry.SheavesOfRings