finite

Mathlib.Data.Fintype.EquivFin

URI: https://scilib.ai/kg/mathlib#Subtype.finite

← MathLib Explorer

English

If α is finite, then any Subtype {x // p x} is finite.

Русский

Если α конечен, то любой подтип {x // p x} конечен.

LaTeX

$$$\operatorname{Finite}(\alpha) \Rightarrow \operatorname{Finite}(\{ x\mid p x\}).$$$

Lean4

/-- This instance also provides `[Finite s]` for `s : Set α`. -/
instance finite {α : Sort*} [Finite α] {p : α → Prop} : Finite { x // p x } :=
  Finite.of_injective Subtype.val Subtype.coe_injective

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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