antitone_lam — Mathlib

English

If for every b, the function a ↦ f(a,b) is antitone, then the function f is antitone in its first argument.

Русский

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

LaTeX

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

Lean4

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

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