sInf — Mathlib

English

If every member I of a set ℐ of ideals is homogeneous, then the infimum sInf ℐ is homogeneous.

Русский

Если каждый идеал I из ℐ однороден, то инфimum этого множества тоже однороден.

LaTeX

$$$(\\forall I \\in \\mathcal{I}, IsHomogeneous(\\mathcal{A}, I)) \\Rightarrow IsHomogeneous(\\mathcal{A}, sInf \\mathcal{I})$$$

Lean4

theorem sInf {ℐ : Set (Ideal A)} (h : ∀ I ∈ ℐ, Ideal.IsHomogeneous 𝒜 I) : (sInf ℐ).IsHomogeneous 𝒜 :=
  by
  rw [sInf_eq_iInf]
  exact iInf₂ h

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