English
For x ∈ α, 1 < height x iff there exist y, z with z < y and y < x.
Русский
Для элемента x высота которого больше 1, существует цепочка y, z ниже x с z < y < x.
LaTeX
$$$$ 1 < \operatorname{height}(x) \iff \exists y, z, \; z < y \land y < x $$$$
Lean4
theorem one_lt_height_iff {x : α} : 1 < Order.height x ↔ ∃ y z, z < y ∧ y < x :=
by
rw [← ENat.add_one_le_iff ENat.one_ne_top, one_add_one_eq_two]
refine ⟨fun h ↦ ?_, ?_⟩
· obtain ⟨p, hp, hlen⟩ := Order.exists_series_of_le_height x (n := 2) h
refine ⟨p 1, p 0, p.rel_of_lt ?_, hp ▸ p.rel_of_lt ?_⟩ <;> simp [Fin.lt_def, hlen]
· rintro ⟨y, z, hzy, hyx⟩
let p : LTSeries α :=
RelSeries.fromListIsChain [z, y, x] (List.cons_ne_nil z [y, x])
(List.IsChain.cons_cons hzy <| List.isChain_pair.mpr hyx)
have : p.last = x := by simp [p, ← RelSeries.getLast_toList]
exact Order.length_le_height this.le
