sSup — Mathlib

English

If every member I of a set ℐ of ideals is homogeneous, then the supremum sSup ℐ is homogeneous.

Русский

Если каждый идеал I в множестве ℐ однородный, то наибольшая верхняя грань sSup ℐ тоже однородна.

LaTeX

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

Lean4

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

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