English
A union of a nonempty chain of ideals of sets is an ideal. If C is a nonempty chain under ⊆ and every I ∈ C is an ideal, then the union ⋃C is an ideal.
Русский
Объединение непустой цепи идеалов — это идеал. Пусть C непустая цепь по включению, и каждый I ∈ C — идеал; тогда ⋃C — идеал.
LaTeX
$$$C \\subseteq \\mathcal{P}(P), \\ IsChain (\\\\subseteq) C \\\\land \\forall I \\in C, IsIdeal I \\\\land C \\neq \\varnothing \\Rightarrow IsIdeal (\\\\bigcup_{I \\in C} I).$$$
Lean4
/-- A union of a nonempty chain of ideals of sets is an ideal. -/
theorem isIdeal_sUnion_of_isChain {C : Set (Set P)} (hidl : ∀ I ∈ C, IsIdeal I) (hC : IsChain (· ⊆ ·) C)
(hNe : C.Nonempty) : IsIdeal C.sUnion :=
isIdeal_sUnion_of_directedOn hidl hC.directedOn hNe
