small_single

Mathlib.Logic.Small.Set

URI: https://scilib.ai/kg/mathlib#small_single

English

A singleton set {x} is small.

Русский

Множество-один элемент {x} малое.

LaTeX

$$$\operatorname{Small}({x})$$$

Lean4

theorem small_single (x : α) : Small.{u} ({ x } : Set α) :=
  inferInstance

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

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

Разделы

Аффилиация

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