English
The equality height a = n holds exactly when a is the minimal element among those with height at least n, i.e., a is the least element whose height is at least n.
Русский
Высота элемента a равна n тогда, когда a является минимальным элементом среди элементов высоты не ниже n.
LaTeX
$$$$ \operatorname{height}(a) = n \iff \operatorname{Minimal}\bigl( \lambda y, \; n \le \operatorname{height}(y) \bigr) a $$$$
Lean4
/-- The elements of finite height `n` are the minimal elements among those of height `≥ n`. -/
theorem height_eq_coe_iff_minimal_le_height {a : α} {n : ℕ} : height a = n ↔ Minimal (fun y => n ≤ height y) a :=
by
by_cases hfin : height a < ⊤
·
cases hn : n with
| zero => simp
| succ => simp [minimal_iff_forall_lt, height_eq_coe_add_one_iff, ENat.add_one_le_iff, coe_lt_height_iff, *]
· suffices ∃ x < a, ↑n ≤ height x by simp_all [minimal_iff_forall_lt]
simp only [not_lt, top_le_iff, height_eq_top_iff] at hfin
obtain ⟨p, rfl, hp⟩ := hfin (n + 1)
use p.eraseLast.last, p.eraseLast_last_rel_last (by cutsat)
simpa [hp] using length_le_height_last (p := p.eraseLast)
