forall — Mathlib

English

Let α be a preorder and β a type. If for every x, the predicate P x y is monotone in y, then the function y ↦ ∀ x, P x y is monotone in y.

Русский

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

LaTeX

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

Lean4

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

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