English
For f: WithTop(α) → β, Monotone f iff Monotone f on α and f x ≤ f ⊤ for all x.
Русский
Для отображения f: WithTop(α) → β, Monotone f эквивалентно тому, что f монотонно на α и f x ≤ f ⊤ для всех x.
LaTeX
$$$$ \\mathrm{Monotone}(f) \\longleftrightarrow \\Big( \\mathrm{Monotone}(f\\circ \\mathrm{coe\_mono}) \\land \\forall x: \\alpha, f x \\le f \\top \\Big). $$$$
Lean4
theorem monotone_iff {f : WithTop α → β} : Monotone f ↔ Monotone (fun (a : α) => f a) ∧ ∀ x : α, f x ≤ f ⊤ :=
⟨fun h => ⟨h.comp WithTop.coe_mono, fun _ => h le_top⟩, fun h =>
WithTop.forall.2
⟨WithTop.forall.2 ⟨fun _ => le_rfl, fun _ h => (not_top_le_coe _ h).elim⟩, fun x =>
WithTop.forall.2 ⟨fun _ => h.2 x, fun _ hle => h.1 (coe_le_coe.1 hle)⟩⟩⟩
