singleton_subset_singleton

Mathlib.Data.Set.Insert

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

English

The singleton {a} is a subset of {b} iff a = b.

Русский

Подмножество {a} ⊆ {b} эквивалентно a = b.

LaTeX

$$$\\{ a \\} \\subseteq \\{ b \\} \\iff a = b$$$

Lean4

theorem singleton_subset_singleton : ({ a } : Set α) ⊆ { b } ↔ a = b := by simp

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

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

Разделы

Аффилиация

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