eq_empty_of_isEmpty

Mathlib.Data.Set.Basic

URI: https://scilib.ai/kg/mathlib#Set.eq_empty_of_isEmpty

English

If α is empty, then any subset s of α is empty.

Русский

Если α пуст, то любой набор s ⊆ α является пустым.

LaTeX

$$$$ [\text{IsEmpty } \alpha] (s) \,\Rightarrow\, s = \emptyset. $$$$

Lean4

theorem eq_empty_of_isEmpty [IsEmpty α] (s : Set α) : s = ∅ :=
  eq_empty_of_subset_empty fun x _ => isEmptyElim x

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

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

Разделы

Аффилиация

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