eq_zero

Mathlib.Data.Set.Insert

URI: https://scilib.ai/kg/mathlib#Set.Nonempty.eq_zero

English

If α has Subsingleton and a zero element 0, then any nonempty subset s of α equals {0}.

Русский

Если α — субодиночка и задан ноль 0, любая непустая подмножество s равно {0}.

LaTeX

$$$s \neq \emptyset \implies s = \{0\}$$$

Lean4

theorem eq_zero [Subsingleton α] [Zero α] {s : Set α} (h : s.Nonempty) : s = {0} :=
  eq_of_nonempty_of_subsingleton' {0} h

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

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

Разделы

Аффилиация

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