English
A nonempty directed union of ideals of sets in a preorder is an ideal. Precisely, if C is a nonempty set of subsets of P such that every member is an ideal and C is directed by inclusion, then the union ⋃C is an ideal.
Русский
Непустое направленное объединение множеств, являющихся идеалами, на частичных упорядочениях, является идеалом. Пусть C ⊆ 2^P, каждый I ∈ C — идеал, и C направленно по включению; тогда ⋃C — идеал.
LaTeX
$$$C \\subseteq \\mathcal{P}(P), \\quad (\\\\forall I \\\\in C, \\\\ IsIdeal I) \\\\land DirectedOn (\\\\subseteq) C \\\\land C \\\\neq \\varnothing \\Rightarrow IsIdeal \\left( \\bigcup_{I \\in C} I \\right).$$$
Lean4
/-- A non-empty directed union of ideals of sets in a preorder is an ideal. -/
theorem isIdeal_sUnion_of_directedOn {C : Set (Set P)} (hidl : ∀ I ∈ C, IsIdeal I) (hD : DirectedOn (· ⊆ ·) C)
(hNe : C.Nonempty) : IsIdeal C.sUnion :=
by
refine
⟨isLowerSet_sUnion (fun I hI ↦ (hidl I hI).1), Set.nonempty_sUnion.2 ?_,
directedOn_sUnion hD (fun J hJ => (hidl J hJ).3)⟩
let ⟨I, hI⟩ := hNe
exact ⟨I, ⟨hI, (hidl I hI).2⟩⟩
