antitone_app — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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