English
Let f be monotone and g be antitone, with f ≤ g. Then for every a,b in the domain, f(a) ≤ g(b).
Русский
Пусть f монотонна, g антитонична, и выполняется неравенство f ≤ g. Тогда для всех a, b в области определения выполняется f(a) ≤ g(b).
LaTeX
$$$ \forall f,g:\alpha\to\beta,\; \text{Monotone}(f) \land \text{Antitone}(g) \land f \le g \Rightarrow \forall m,n:\alpha,\ f(m) \le g(n).$$
Lean4
/-- If `f` is monotone, `g` is antitone, and `f ≤ g`, then for all `a`, `b` we have `f a ≤ g b`. -/
theorem forall_le_of_antitone {β : Type*} [Preorder β] {f g : α → β} (hf : Monotone f) (hg : Antitone g) (h : f ≤ g)
(m n : α) : f m ≤ g n :=
calc
f m ≤ f (m ⊔ n) := hf le_sup_left
_ ≤ g (m ⊔ n) := (h _)
_ ≤ g n := hg le_sup_right
