English
Given a set of primary ideals whose infimum is I, there exists a subfamily whose members are pairwise with distinct radicals (no two have equal radical).
Русский
Если дано семейство первичных идеалов с Inf = I, существует подсемейство, члены которого образуют попарно различные радикалы.
LaTeX
$$∃ t, t.inf id = I ∧ ∀ J ∈ t, J.IsPrimary ∧ (t : Set).Pairwise (≠ on radical)$$
Lean4
theorem decomposition_erase_inf [DecidableEq (Ideal R)] {I : Ideal R} {s : Finset (Ideal R)} (hs : s.inf id = I) :
∃ t : Finset (Ideal R), t ⊆ s ∧ t.inf id = I ∧ (∀ ⦃J⦄, J ∈ t → ¬(t.erase J).inf id ≤ J) := by
induction s using Finset.eraseInduction with
| H s IH =>
by_cases H : ∀ J ∈ s, ¬(s.erase J).inf id ≤ J
· exact ⟨s, Finset.Subset.rfl, hs, H⟩
push_neg at H
obtain ⟨J, hJ, hJ'⟩ := H
refine (IH _ hJ ?_).imp fun t ↦ And.imp_left (fun ht ↦ ht.trans (Finset.erase_subset _ _))
rw [← Finset.insert_erase hJ] at hs
simp [← hs, hJ']
