coheight_eq_iSup_gt_coheight — Mathlib

English

For all x, coheight x = ⨆ y > x, coheight y + 1.

Русский

Для всего x выполняется coheight x = ⨆ y > x, coheight y + 1.

LaTeX

$$$ \operatorname{coheight}(x) = \bigsqcup_{y > x} (\operatorname{coheight}(y) + 1) $$$

Lean4

/-- Another characterization of coheight, based on the supremum of the coheights of elements above.
-/
theorem coheight_eq_iSup_gt_coheight (x : α) : coheight x = ⨆ y > x, coheight y + 1 :=
  height_eq_iSup_lt_height (α := αᵒᵈ) x

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