English
Let x ∈ α with height x < ⊤. Then for every n ∈ ℕ, n < height x iff ∃ y < x with height y = n.
Русский
Пусть x ∈ α и высота x меньше верхнего предела. Тогда для любого n ∈ ℕ верно: n < height(x) тогда и только если существует y < x такое, что height(y) = n.
LaTeX
$$$$ (\operatorname{height}(x) < \top) \implies ( n < \operatorname{height}(x) \iff \exists y < x, \operatorname{height}(y) = n) $$$$
Lean4
theorem coe_lt_height_iff {x : α} {n : ℕ} (hfin : height x < ⊤) : n < height x ↔ ∃ y < x, height y = n
where
mp
h := by
obtain ⟨m, hx : height x = m⟩ := Option.ne_none_iff_exists'.mp hfin.ne_top
rw [hx] at h; norm_cast at h
obtain ⟨p, hp, hlen⟩ := exists_series_of_height_eq_coe x hx
use p ⟨n, by omega⟩
constructor
· rw [← hp]
apply LTSeries.strictMono
simp [Fin.last]; omega
· exact height_eq_index_of_length_eq_height_last (by simp [hlen, hp, hx]) ⟨n, by omega⟩
mpr := fun ⟨y, hyx, hy⟩ => hy ▸ height_strictMono hyx (lt_of_le_of_lt (height_mono hyx.le) hfin)
