exists_ne_bot

Mathlib.Order.WithBot

URI: https://scilib.ai/kg/mathlib#WithBot.exists_ne_bot

English

(∃ x ≠ ⊥, p x) ↔ ∃ x : α, p x.

Русский

(Существует x ≠ ⊥, p x) эквивалентно ∃ x ∈ α, p x.

LaTeX

$$$(\exists x \neq ⊥, p x) \iff \exists x : α, p x$$$

Lean4

theorem exists_ne_bot {p : WithBot α → Prop} : (∃ x ≠ ⊥, p x) ↔ ∃ x : α, p x := by simp [ne_bot_iff_exists]

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

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

Разделы

Аффилиация

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