head_map — Mathlib

English

Head of the mapped LTSeries equals applying f to the 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

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

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