optionEquiv — Mathlib

English

If C is finite, then WithTerminal C is finite, via the option-equivalence with Option C.

Русский

Если C конечен, то и WithTerminal C конечен, через эквивалентность с Option C.

LaTeX

$$instFintype [Fintype C] : Fintype (WithTerminal C)$$

Lean4

/-- The equivalence between `Option C` and `WithTerminal C` (they are both the
type `C` plus an extra object `none` or `star`). -/
def optionEquiv : Option C ≃ WithTerminal C
    where
  toFun
    | some a => of a
    | none => star
  invFun
    | of a => some a
    | star => none
  left_inv a := by cases a <;> simp
  right_inv a := by cases a <;> simp

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