ball — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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