forall — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem «forall» {P : β → α → Prop} (hP : ∀ x, Antitone (P x)) : Antitone fun y => ∀ x, P x y := fun _ _ hy h x =>
  hP x hy (h x)

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