forall

Mathlib.Order.WithBot

URI: https://scilib.ai/kg/mathlib#WithTop.forall

English

For any p : WithTop α → Prop, (∀ x, p x) is equivalent to p ⊤ ∧ ∀ x : α, p x.

Русский

Для любого p : WithTop α → Prop, выполняется равенство: ∀ x, p x ⇔ p ⊤ ∧ ∀ x ∈ α, p x.

LaTeX

$$$(\forall x, p x) \iff p(\top) \land \forall x : α, p x$$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru