English
If f: α → β is surjective and strictly comonotonic, a LTSeries in β can be pulled back to a LTSeries in α.
Русский
Если f: α → β сюрьективна и строго комонотонна, цепь LTSeries в β может быть перетянута обратно в α.
LaTeX
$$$\forall {\alpha}\ {\beta} [Preorder\alpha] [Preorder\beta] (p: LTSeries\beta) (f: \alpha \to \beta) (comap : \forall ⦃x y⦄, f x < f y \Rightarrow x < y) (surjective : Function.Surjective f), LTSeries\alpha$$$
Lean4
/-- For two preorders `α, β`, if `f : α → β` is surjective and strictly comonotonic, then a
strict series of `β` can be pulled back to a strict chain of `α` by
`b₀ < b₁ < ... < bₙ ↦ f⁻¹ b₀ < f⁻¹ b₁ < ... < f⁻¹ bₙ` where `f⁻¹ bᵢ` is an arbitrary element in the
preimage of `f⁻¹ {bᵢ}`.
-/
@[simps!]
noncomputable def comap (p : LTSeries β) (f : α → β) (comap : ∀ ⦃x y⦄, f x < f y → x < y)
(surjective : Function.Surjective f) : LTSeries α :=
mk p.length (fun i ↦ (surjective (p i)).choose)
(fun i j h ↦ comap (by simpa only [(surjective _).choose_spec] using p.strictMono h))
