last_map — Mathlib

English

Last of the mapped LTSeries equals applying f to the last.

Русский

Последний элемент отображённой LTSeries равен применению 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

@[simp]
theorem last_map (p : LTSeries α) (f : α → β) (hf : StrictMono f) : (p.map f hf).last = f p.last :=
  rfl

Похожие утверждения