notMem_empty

Mathlib.Data.Finset.Empty

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

English

For every a, a is not a member of the empty Finset.

Русский

Для любого a: A не принадлежит пустому Finset.

LaTeX

$$$a \\\\notin (\\\\emptyset : Finset\\\\alpha)$$$

Lean4

@[simp, grind]
theorem notMem_empty (a : α) : a ∉ (∅ : Finset α) := by simp only [mem_def, empty_val, notMem_zero, not_false_iff]

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

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

Разделы

Аффилиация

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