eq_empty_of_forall_notMem

Mathlib.Data.Finset.Empty

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

English

If no element belongs to s, then s = ∅.

Русский

Если никакой элемент не принадлежит s, то s = ∅.

LaTeX

$$$(\\\\forall x, x \\\\notin s) \\\\Rightarrow s = \\\\emptyset$$$

Lean4

theorem eq_empty_of_forall_notMem {s : Finset α} (H : ∀ x, x ∉ s) : s = ∅ :=
  eq_of_veq (eq_zero_of_forall_notMem H)

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

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

Разделы

Аффилиация

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