fintypeOfOptionEquiv

Mathlib.Data.Fintype.Option

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

← MathLib Explorer

English

If α is finite and α ≃ Option β, then β is finite.

Русский

Если α конечно и α ≃ Option β, то β конечно.

LaTeX

$$$\alpha \text{ finite} \land (\alpha \simeq Option\;\beta) \Rightarrow \text{Finite}(\beta)$$$

Lean4

/-- A type is a `Fintype` if its successor (using `Option`) is a `Fintype`. -/
def fintypeOfOptionEquiv [Fintype α] (f : α ≃ Option β) : Fintype β :=
  haveI := Fintype.ofEquiv _ f
  fintypeOfOption

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

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

Разделы

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

Аффилиация

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