forall — Mathlib

English

For any predicate p on OnePoint X, ∀x, p x holds iff p(∞) holds and ∀x ∈ X, p(Some x) holds.

Русский

Для любого предиката p на OnePoint X справедливо: ∀x, p x тогда и только тогда, когда p(∞) и ∀x∈X, p(Some x).

LaTeX

$$$\\forall p:\\mathrm{OnePoint}~X \\to \\mathrm{Prop},\\; (\\forall x:\\mathrm{OnePoint}~X, p\\,x) \\iff p(\\infty) \\land (\\forall x:X, p(\\mathrm{OnePoint.some}\\ x))$$$

Lean4

protected theorem «forall» {p : OnePoint X → Prop} : (∀ (x : OnePoint X), p x) ↔ p ∞ ∧ ∀ (x : X), p x :=
  Option.forall

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