English
For x ∈ α and n ∈ ℕ, height x = n + 1 iff height x < ⊤ and (∃ y < x with height y = n) and (∀ y < x, height y ≤ n).
Русский
Пусть x ∈ α и n ∈ ℕ. Тогда height(x) = n + 1 если и только если height(x) < ⊤ и существует y < x с height(y) = n, и для всех y < x выполняется height(y) ≤ n.
LaTeX
$$$$ \operatorname{height}(x) = n + 1 \iff \big( \operatorname{height}(x) < \top \land (\exists y < x, \operatorname{height}(y) = n) \land (\forall y < x, \operatorname{height}(y) \le n) \big) $$$$
Lean4
theorem height_eq_coe_add_one_iff {x : α} {n : ℕ} :
height x = n + 1 ↔ height x < ⊤ ∧ (∃ y < x, height y = n) ∧ (∀ y < x, height y ≤ n) :=
by
wlog hfin : height x < ⊤
· simp_all
exact ne_of_beq_false rfl
simp only [hfin, true_and]
trans n < height x ∧ height x ≤ n + 1
· rw [le_antisymm_iff, and_comm]
simp [ENat.add_one_le_iff]
· congr! 1
· exact coe_lt_height_iff hfin
· simpa [hfin, ENat.lt_add_one_iff] using height_le_coe_iff (x := x) (n := n + 1)
