English
For f: WithBot α → β, Monotone f iff Monotone (λ a, f a) and ∀ x:α, f(⊥) ≤ f x.
Русский
Для f: WithBot α → β, Monotone f эквивалентно Monotone (λ a, f a) и ∀ x:α, f(⊥) ≤ f x.
LaTeX
$$$ \text{Monotone } f \iff \big( \text{Monotone } ( \lambda a: \alpha, f(a) ) \land \forall x: \alpha, f(\bot) \le f(x) \big)$$$
Lean4
theorem monotone_iff {f : WithBot α → β} : Monotone f ↔ Monotone (fun a ↦ f a : α → β) ∧ ∀ x : α, f ⊥ ≤ f x :=
⟨fun h ↦ ⟨h.comp WithBot.coe_mono, fun _ ↦ h bot_le⟩, fun h ↦
WithBot.forall.2
⟨WithBot.forall.2 ⟨fun _ => le_rfl, fun x _ => h.2 x⟩, fun _ =>
WithBot.forall.2 ⟨fun h => (not_coe_le_bot _ h).elim, fun _ hle => h.1 (coe_le_coe.1 hle)⟩⟩⟩
