English
For f: WithBot α → β, StrictMono f iff StrictMono (λ a, f a) and ∀ x: α, f ⊥ < f x.
Русский
Для f: WithBot α → β, StrictMono f эквивалентно StrictMono (λ a, f a) и ∀ x: α, f(⊥) < f(x).
LaTeX
$$$ \text{StrictMono } f \iff \big( \text{StrictMono } ( \lambda a: \alpha, f(a) ) \land \forall x: \alpha, f(\bot) < f(x) \big)$$$
Lean4
theorem strictMono_iff {f : WithBot α → β} : StrictMono f ↔ StrictMono (fun a => f a : α → β) ∧ ∀ x : α, f ⊥ < f x :=
⟨fun h => ⟨h.comp WithBot.coe_strictMono, fun _ => h (bot_lt_coe _)⟩, fun h =>
WithBot.forall.2
⟨WithBot.forall.2 ⟨flip absurd (lt_irrefl _), fun x _ => h.2 x⟩, fun _ =>
WithBot.forall.2 ⟨fun h => (not_lt_bot h).elim, fun _ hle => h.1 (coe_lt_coe.1 hle)⟩⟩⟩
