coheight_eq_coe_add_one_iff — Mathlib

English

For x with coheight x < ⊤, the equality coheight x = n + 1 holds iff coheight x < ⊤ and (∃ y > x with coheight y = n) and (∀ y > x, coheight y ≤ n).

Русский

Для x с coheight(x) < ⊤ истинно coheight(x) = n + 1 тогда и только тогда, когда coheight(x) < ⊤ и (∃ y > x, coheight(y) = n) и (∀ y > x, coheight(y) ≤ n).

LaTeX

$$$$ \operatorname{coheight}(x) = n + 1 \iff \big( \operatorname{coheight}(x) < \top \land (\exists y > x, \operatorname{coheight}(y) = n) \land (\forall y > x, \operatorname{coheight}(y) \le n) \big) $$$$

Lean4

theorem coheight_eq_coe_add_one_iff {x : α} {n : ℕ} :
    coheight x = n + 1 ↔ coheight x < ⊤ ∧ (∃ y > x, coheight y = n) ∧ (∀ y > x, coheight y ≤ n) :=
  height_eq_coe_add_one_iff (α := αᵒᵈ)

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