exists

Mathlib.Order.WithBot

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

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

$$$(\exists x, p x) \iff p(\top) \lor \exists x : α, p x$$$

Lean4

protected theorem «exists» {p : WithTop α → Prop} : (∃ x, p x) ↔ p ⊤ ∨ ∃ x : α, p x :=
  Option.exists

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

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

Разделы

Аффилиация

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