forall — Mathlib

English

For any predicate p on ULift α, the universal quantification over ULift α is equivalent to the universal quantification over α applied to up.

Русский

Для произвольного предиката p на ULift α справедливо: ∀ x : ULift α, p x равносильно ∀ a : α, p(ULift.up a).

LaTeX

$$$\\forall x : ULift\\,\\alpha\\, p\\,x \\iff \\forall a : \\alpha,\\, p(\\mathrm{up}(a))$$$

Lean4

@[simp]
theorem «forall» {p : ULift α → Prop} : (∀ x, p x) ↔ ∀ x : α, p (ULift.up x) :=
  up_surjective.forall

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