English
As above, (p.map f hf).last = f p.last.
Русский
Аналогично, последний элемента отображённой последовательности равен применению f к последнему исходной.
LaTeX
$$$\forall {\alpha}\ {\beta} [Preorder\alpha] [Preorder\beta] (p: LTSeries\alpha) (f: \alpha \to \beta) (hf: StrictMono f), (p.map f hf).last = f(p.last)$$$
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_int (p : LTSeries ℤ) (i j : Fin (p.length + 1)) (hij : i ≤ j) :
p i + j ≤ p j + i := by
-- The proof is identical to `LTSeries.apply_add_index_le_apply_add_index_nat`, but seemed easier
-- to copy rather than to abstract
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
