English
If p is a LTSeries α and f: α → β is strictly monotone, then p.map f hf is a LTSeries β with toFun = f ∘ p.toFun and strictly monotone = hf ∘ p.strictMono.
Русский
Если p — LTSeries α и f: α → β строго монотонна, то p.map f hf является LTSeries β с toFun = f ∘ p.toFun и строгим монотонным = hf ∘ p.strictMono.
LaTeX
$$$\forall {\alpha}\ {\beta} [Preorder\alpha] [Preorder\beta] (p: LTSeries\alpha) (f: \alpha \to \beta) (hf: StrictMono f), (p.map f hf) = LTSeries.mk p.length (f \circ p.toFun) (hf \circ p.strictMono)$$$
Lean4
/-- For two preorders `α, β`, if `f : α → β` is strictly monotonic, then a strict chain of `α`
can be pushed out to a strict chain of `β` by
`a₀ < a₁ < ... < aₙ ↦ f a₀ < f a₁ < ... < f aₙ`
-/
@[simps!]
def map (p : LTSeries α) (f : α → β) (hf : StrictMono f) : LTSeries β :=
LTSeries.mk p.length (f.comp p) (hf.comp p.strictMono)
