eq_one

Mathlib.Data.Set.Insert

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

English

If α has Subsingleton and a unity 1, then any nonempty subset s of α equals {1}.

Русский

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

LaTeX

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

Lean4

theorem eq_one [Subsingleton α] [One α] {s : Set α} (h : s.Nonempty) : s = { 1 } :=
  eq_of_nonempty_of_subsingleton' { 1 } h

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

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

Разделы

Аффилиация

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