coheight_eq_coe_iff — Mathlib

English

Let x ∈ α and n ∈ ℕ. Then coheight x = n + 1 iff coheight x < ⊤ and (∃ y > x with coheight y = n) and (∀ y > x, coheight y ≤ n).

Русский

Пусть x ∈ α и n ∈ ℕ. Тогда 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_iff {x : α} {n : ℕ} :
    coheight x = n ↔ coheight x < ⊤ ∧ (n = 0 ∨ ∃ y > x, coheight y = n - 1) ∧ (∀ y > x, coheight y < n) :=
  height_eq_coe_iff (α := αᵒᵈ)

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