forall — Mathlib

English

For any predicate p on WithBot α, (∀ x, p x) holds iff p at bottom and ∀ a, p a holds.

Русский

Для любого предиката p на WithBot α, выполняется (∀ x, p x) эквивалентно p нижнему элементу и для всех a: p a.

LaTeX

$$$\\forall {p:WithBot α \\to Prop}, (\\forall x, p x) \\iff p(\\bot) \\wedge (\\forall x:α, p x)$$$

Lean4

protected theorem «forall» {p : WithBot α → Prop} : (∀ x, p x) ↔ p ⊥ ∧ ∀ x : α, p x :=
  Option.forall

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