English
There exists a maximal irreducible set containing a given irreducible set, obtained via Zorn’s Lemma.
Русский
Существует максимальное неразложимое множество, содержащее данное неразложимое множество, получаемое с помощью леммы Зорно.
LaTeX
$$$\\exists t : Set X, \\operatorname{IsPreirreducible}(t) \\land s \\subseteq t \\land \\forall u, \\operatorname{IsPreirreducible}(u) \\rightarrow t \\subseteq u \\rightarrow u = t$$$
Lean4
theorem exists_preirreducible (s : Set X) (H : IsPreirreducible s) :
∃ t : Set X, IsPreirreducible t ∧ s ⊆ t ∧ ∀ u, IsPreirreducible u → t ⊆ u → u = t :=
let ⟨m, hsm, hm⟩ :=
zorn_subset_nonempty {t : Set X | IsPreirreducible t}
(fun c hc hcc _ =>
⟨⋃₀ c, fun u v hu hv ⟨y, hy, hyu⟩ ⟨x, hx, hxv⟩ =>
let ⟨p, hpc, hyp⟩ := mem_sUnion.1 hy
let ⟨q, hqc, hxq⟩ := mem_sUnion.1 hx
Or.casesOn (hcc.total hpc hqc)
(fun hpq : p ⊆ q =>
let ⟨x, hxp, hxuv⟩ := hc hqc u v hu hv ⟨y, hpq hyp, hyu⟩ ⟨x, hxq, hxv⟩
⟨x, mem_sUnion_of_mem hxp hqc, hxuv⟩)
fun hqp : q ⊆ p =>
let ⟨x, hxp, hxuv⟩ := hc hpc u v hu hv ⟨y, hyp, hyu⟩ ⟨x, hqp hxq, hxv⟩
⟨x, mem_sUnion_of_mem hxp hpc, hxuv⟩,
fun _ hxc => subset_sUnion_of_mem hxc⟩)
s H
⟨m, hm.prop, hsm, fun _u hu hmu => (hm.eq_of_subset hu hmu).symm⟩
