ball — Mathlib

English

If for every x ∈ s the predicate P x y is monotone in y, then the function y ↦ ∀ x ∈ s, P x y is monotone in y.

Русский

Если для каждого x ∈ s предикат P x y монотонен по y, то функция y ↦ ∀ x ∈ s, P x y монотонна.

LaTeX

$$$\\\\forall y,z\\\\in \\\\alpha,\\\\ y \\\\le z \\\\Rightarrow (\\\\forall x\\\\in s, P x y) \\\\Rightarrow (\\\\forall x\\\\in s, P x z)$$$

Lean4

theorem ball {P : β → α → Prop} {s : Set β} (hP : ∀ x ∈ s, Monotone (P x)) : Monotone fun y => ∀ x ∈ s, P x y :=
  fun _ _ hy h x hx => hP x hx hy (h x hx)

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