exists_mem_empty_iff

Mathlib.Data.Finset.Empty

URI: https://scilib.ai/kg/mathlib#Finset.exists_mem_empty_iff

English

There is no x with x ∈ ∅ and p(x) for any predicate p.

Русский

Не существует x such that x ∈ ∅ и p(x) для любого p.

LaTeX

$$$ (\exists x, x \in (\emptyset : \mathrm{Finset}\, \alpha) \land p(x)) \iff \mathrm{False} $$$

Lean4

theorem exists_mem_empty_iff (p : α → Prop) : (∃ x, x ∈ (∅ : Finset α) ∧ p x) ↔ False := by grind

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

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

Разделы

Аффилиация

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