homogeneousHull_eq_sInf — Mathlib

English

The hull equals the infimum over all homogeneous ideals J with I ≤ J.toIdeal: Ideal.homogeneousHull 𝒜 I = sInf { J : HomogeneousIdeal 𝒜 | I ≤ J.toIdeal }.

Русский

Оболочка равна инфимууму по всем однородным идеалам J, удовлетворяющим I ≤ J.toIdeal: Ideal.homogeneousHull 𝒜 I = sInf { J : HomogeneousIdeal 𝒜 | I ≤ J.toIdeal }.

LaTeX

$$$ \text{Ideal.homogeneousHull } 𝒜 I = \inf \{ J : HomogeneousIdeal 𝒜 \mid I \le J.toIdeal \} $$$

Lean4

theorem homogeneousHull_eq_sInf (I : Ideal A) :
    Ideal.homogeneousHull 𝒜 I = sInf {J : HomogeneousIdeal 𝒜 | I ≤ J.toIdeal} :=
  Eq.symm <| IsGLB.sInf_eq <| (Ideal.homogeneousHull.gc 𝒜).isLeast_l.isGLB

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