English
As above, (p.map f hf).head = f p.head.
Русский
Аналогично, голова отображённой последовательности равна применению f к голове исходной.
LaTeX
$$$\forall {\alpha}\ {\beta} [Preorder\alpha] [Preorder\beta] (p: LTSeries\alpha) (f: \alpha \to \beta) (hf: StrictMono f), (p.map f hf).head = f(p.head)$$$
Lean4
/-- In ℕ, two entries in an `LTSeries` differ by at least the difference of their indices.
(Expressed in a way that avoids subtraction).
-/
theorem apply_add_index_le_apply_add_index_nat (p : LTSeries ℕ) (i j : Fin (p.length + 1)) (hij : i ≤ j) :
p i + j ≤ p j + i := by
have ⟨i, hi⟩ := i
have ⟨j, hj⟩ := j
simp only [Fin.mk_le_mk] at hij
simp only at *
induction j, hij using Nat.le_induction with
| base => simp
| succ j _hij ih =>
specialize ih (Nat.lt_of_succ_lt hj)
have step : p ⟨j, _⟩ < p ⟨j + 1, _⟩ := p.step ⟨j, by cutsat⟩
norm_cast at *; cutsat
