forall — Mathlib

English

For any property p on PLift α, all PLift elements satisfy p if and only if all α-elements satisfy p after lifting.

Русский

Для любого свойства p на PLift α верно: для всех x в PLift α p(x) эквивалентно для всех a в α p(up(a)).

LaTeX

$$$\\forall {p : \\mathrm{PLift} \\alpha \\rightarrow \\mathrm{Prop}}, \\bigl(\\forall x \\in \\mathrm{PLift} \\alpha, p(x)\\bigr) \\Leftrightarrow \\bigl(\\forall x : \\alpha, p(\\mathrm{up}(x))\\bigr)$$$

Lean4

theorem «forall» {p : PLift α → Prop} : (∀ x, p x) ↔ ∀ x : α, p (PLift.up x) :=
  up_surjective.forall

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