iInf — Mathlib

English

If a family of ideals (f i) consists of homogeneous ideals, then their infimum ⨅ i f i is homogeneous.

Русский

Если семейство идеалов (f_i) состоит из однородных идеалов, то их infimum ⨅ i f_i тоже однороден.

LaTeX

$$$(\\forall i, IsHomogeneous(\\mathcal{A}, f(i))) \\Rightarrow IsHomogeneous(\\mathcal{A}, \\big(\\bigwedge_i f(i)\\big))$$$

Lean4

protected theorem iInf {κ : Sort*} {f : κ → Ideal A} (h : ∀ i, (f i).IsHomogeneous 𝒜) : (⨅ i, f i).IsHomogeneous 𝒜 :=
  by
  intro i x hx
  simp only [Ideal.mem_iInf] at hx ⊢
  exact fun j => h _ _ (hx j)

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