fintypeOfOption

Mathlib.Data.Fintype.Option

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

← MathLib Explorer

English

If Option α is finite, then α is finite.

Русский

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

LaTeX

$$[Fintype (Option α)] ⇒ Fintype α$$

Lean4

/-- If `Option α` is a `Fintype` then so is `α` -/
def fintypeOfOption {α : Type*} [Fintype (Option α)] : Fintype α :=
  ⟨Finset.eraseNone (Fintype.elems (α := Option α)), fun x => mem_eraseNone.mpr (Fintype.complete (some x))⟩

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

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

Разделы

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

Аффилиация

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