radical_iInf_le — Mathlib

English

For a family I(i) of ideals, radical of the infimum is less than or equal to the infimum of radicals.

Русский

Для семейства I(i) идеалов радикал их infimum меньше или равен infimum радикалов.

LaTeX

$$$\\operatorname{radical}\\left(\\bigwedge_i I(i)\\right) \\le \\bigwedge_i \\operatorname{radical}(I(i))$$$

Lean4

/-- The reverse inclusion does not hold for e.g. `I := fun n : ℕ ↦ Ideal.span {(2 ^ n : ℤ)}`. -/
theorem radical_iInf_le {ι} (I : ι → Ideal R) : radical (⨅ i, I i) ≤ ⨅ i, radical (I i) :=
  le_iInf fun _ ↦ radical_mono (iInf_le _ _)

Похожие утверждения