chainBotCoeff_eq_sSup — Mathlib

English

The chain bottom coefficient equals the supremum of the set {−k | P.root j − k•P.root i ∈ range P.root} with a cast.

Русский

Цепной нижний коэффициент равен супремусу множества {−k | P.root j − k•P.root i ∈ range P.root} (с преобразованиями).

LaTeX

$$chainBotCoeff i j = sSup {k | P.root j - k • P.root i ∈ range P.root}$$

Lean4

theorem chainBotCoeff_eq_sSup : P.chainBotCoeff i j = sSup {k | P.root j - k • P.root i ∈ range P.root} := by
  rw [← Iic_chainBotCoeff_eq h, csSup_Iic]

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