English
If a finite set of ideals s has infimum equal to I, there exists a subcollection t ⊆ s with the same infimum I, and such that no member is redundant with respect to the infimum.
Русский
Если конечный набор идеалов s имеетInf равный I, существует подмножество t ⊆ s с тем же Inf = I, и никакой элемент не является избыточным по отношению к Inf.
LaTeX
$$∃ t ⊆ s, t.inf id = I ∧ ∀ J ∈ t, ¬(t.erase J).inf id ≤ J$$
Lean4
/-- A ring `R` satisfies `IsLasker R` when any `I : Ideal R` can be decomposed into
finitely many primary ideals. -/
def IsLasker : Prop :=
∀ I : Ideal R, ∃ s : Finset (Ideal R), s.inf id = I ∧ ∀ ⦃J⦄, J ∈ s → J.IsPrimary
