coheight_coe_withTop — Mathlib

English

The coheight increases by one when passing to WithTop via the dual construction: coheight (x : WithTop α) = coheight x + 1.

Русский

Соотношение высоты-длины обратного порядка увеличивается на единицу при переходе к WithTop: coheight (x : WithTop α) = coheight x + 1.

LaTeX

$$$$\\operatorname{coheight}(x : \\mathrm{WithTop}\\, \\alpha) = \\operatorname{coheight}(x) + 1.$$$$

Lean4

@[simp]
theorem coheight_coe_withTop (x : α) : coheight (x : WithTop α) = coheight x + 1 :=
  height_coe_withBot (α := αᵒᵈ) x

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