instInfiniteOption

Mathlib.Data.Fintype.EquivFin

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

English

If α is infinite, then the option type with α is infinite.

Русский

Пусть α бесконечен. Тогда тип Option α бесконечен.

LaTeX

$$$ \\forall \\alpha\\ (\\operatorname{Infinite}(\\alpha) \\Rightarrow \\operatorname{Infinite}(\\mathrm{Option}\\,\\alpha)) $$$

Lean4

instance [Infinite α] : Infinite (Option α) :=
  Infinite.of_injective some (Option.some_injective α)

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

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

Разделы

Аффилиация

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