subsingleton

Mathlib.Data.Part

URI: https://scilib.ai/kg/mathlib#Part.subsingleton

English

For any Part α, the set {a | a ∈ o} is subsingleton.

Русский

Для любого Part α множество {a | a ∈ o} является подсингуотоном.

LaTeX

$$$$\mathrm{Part}.\mathrm{subsingleton}(o) : \;\mathrm{Set.Subsingleton}\{a \mid a \in o\}.$$$$

Lean4

protected theorem subsingleton (o : Part α) : Set.Subsingleton {a | a ∈ o} := fun _ ha _ hb => mem_unique ha hb

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

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

Разделы

Аффилиация

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