monotone_iff_apply₂ — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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