monotone_app — Mathlib

English

If f : β → α → γ is monotone in its second argument for a fixed first argument, then the function a ↦ f(b,a) is monotone.

Русский

Если f : β → α → γ монотонна по второму аргументу для фиксированного первого, тогда функция a ↦ f(b,a) монотонна.

LaTeX

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

Lean4

theorem monotone_app (f : β → α → γ) (b : β) (hf : Monotone fun a b ↦ f b a) : Monotone (f b) := fun _ _ h ↦ hf h b

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