coheight_coe_withBot — Mathlib

English

Let α be a preorder. For any x in α, the coheight of x when viewed inside WithBot α equals the coheight of x in α itself. In other words, embedding α into WithBot α does not change the coheight of elements.

Русский

Пусть α — частично упорядоченное множество. Для любого элемента x из α ко-высота x при рассмотрении внутри WithBot α равна ко-высоте x в α; то есть внедрение α в WithBot α не изменяет ко-высоту элементов.

LaTeX

$$$\\forall x:\\alpha,\\; \\operatorname{coheight}(x:\\WithBot\\alpha) = \\operatorname{coheight}(x).$$$

Lean4

@[simp]
theorem coheight_coe_withBot (x : α) : coheight (x : WithBot α) = coheight x :=
  height_coe_withTop (α := αᵒᵈ) x

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