toFinite

Mathlib.Data.Finite.Defs

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

English

If a Set has a Finite instance, then it is finite.

Русский

Если у множества есть экземпляр Finite, значит оно конечное.

LaTeX

$$$[\\text{Finite } s] \\Rightarrow s.Finite$$$

Lean4

/-- Constructor for `Set.Finite` using a `Finite` instance. -/
theorem toFinite (s : Set α) [Finite s] : s.Finite :=
  ‹_›

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

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

Разделы

Аффилиация

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