monotone_lam — Mathlib

English

If for every b, the function a ↦ f(a,b) is monotone, then the function f is monotone in both arguments.

Русский

Если для каждого b функция a ↦ f(a,b) монотонна, то функция f монотонна по обеим аргументам.

LaTeX

$$$\\bigl(\\forall b,\\mathrm{Monotone}(\\lambda a. f(a,b))\\bigr)\\Rightarrow \\mathrm{Monotone}(f)$$$

Lean4

theorem monotone_lam {f : α → β → γ} (hf : ∀ b, Monotone fun a ↦ f a b) : Monotone f := fun _ _ h b ↦ hf b h

Похожие утверждения