insertNone — Mathlib

English

Inserting an Option.none into a finite enumeration yields an enumeration of Option α.

Русский

Вставка None в перечисление FinEnum даёт перечисление Option α.

LaTeX

$$$\\operatorname{insertNone}(\\alpha) : Fin (card\\ α + 1) \\to FinEnum (Option α)$$$

Lean4

/-- Inserting an `Option.none` anywhere in an enumeration yields another enumeration. -/
def insertNone (α : Type u) [FinEnum α] (i : Fin (card α + 1)) : FinEnum (Option α)
    where
  card := card α + 1
  equiv := equiv.optionCongr.trans <| finSuccEquiv' i |>.symm

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