antitone_iff_apply₂ — Mathlib

English

Let f : α → ∀ i, β i. Then f is antitone iff for every i, the function x ↦ f x i is antitone.

Русский

Пусть f : α → ∀ i, β i. Тогда f антимонотонна тогда, когда для каждого i функция x ↦ f x i антимонотонна.

LaTeX

$$$\mathrm{Antitone}(f) \iff \forall i,\ \mathrm{Antitone}(x \mapsto f x i)$$$

Lean4

theorem antitone_iff_apply₂ : Antitone f ↔ ∀ i, Antitone (f · i) := by simp [Antitone, Pi.le_def, @forall_swap ι]

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