coe_lt_coheight_iff — Mathlib

English

Let x with coheight x < ⊤. Then for every n ∈ ℕ, n < coheight x iff ∃ y > x with coheight y = n.

Русский

Пусть x удовлетворяет coheight(x) < ⊤. Тогда для любого n ∈ ℕ верно: n < coheight(x) тогда и только если существует y > x такое, что coheight(y) = n.

LaTeX

$$$$ (\operatorname{coheight}(x) < \top) \implies ( n < \operatorname{coheight}(x) \iff \exists y > x, \operatorname{coheight}(y) = n) $$$$

Lean4

theorem coe_lt_coheight_iff {x : α} {n : ℕ} (hfin : coheight x < ⊤) : n < coheight x ↔ ∃ y > x, coheight y = n :=
  coe_lt_height_iff (α := αᵒᵈ) hfin

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