English
StrictMono f iff StrictMono on α and ∀ x, f x < f ⊤.
Русский
StrictMono f тогда и только тогда, когда f ограничено на α строго возрастает и ∀ x, f x < f ⊤.
LaTeX
$$$$ \\text{StrictMono}(f) \\iff \\Big( \\text{StrictMono}(\\lambda a: \\alpha, f a) \\land \\forall x: \\alpha, f x < f \\top \\Big). $$$$
Lean4
theorem strictMono_iff {f : WithTop α → β} : StrictMono f ↔ StrictMono (fun (a : α) => f a) ∧ ∀ x : α, f x < f ⊤ :=
⟨fun h => ⟨h.comp WithTop.coe_strictMono, fun _ => h (coe_lt_top _)⟩, fun h =>
WithTop.forall.2
⟨WithTop.forall.2 ⟨flip absurd (lt_irrefl _), fun _ h => (not_top_lt h).elim⟩, fun x =>
WithTop.forall.2 ⟨fun _ => h.2 x, fun _ hle => h.1 (coe_lt_coe.1 hle)⟩⟩⟩
