of_subsingleton

Mathlib.Data.Set.Finite.Basic

URI: https://scilib.ai/kg/mathlib#Set.Finite.of_subsingleton

English

If the ambient type α is a subsingleton, then any subset s ⊆ α is finite.

Русский

Если тип α является подсингелтон, то любое подмножество s ⊆ α конечное.

LaTeX

$$$[Subsingleton\,\alpha] \forall s : Set\alpha, Finite s$$$

Lean4

@[nontriviality]
theorem of_subsingleton [Subsingleton α] (s : Set α) : s.Finite :=
  s.toFinite

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

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

Разделы

Аффилиация

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