English
There is an induction principle for finite types: any finite type is, up to an Equiv, either Empty or Option α.
Русский
Существующий принцип индукции по конечным типам: любой конечный тип эквивалентен либо пустому, либо Option α.
LaTeX
$$$\\forall P:\\text{Type} \\to \\Prop,\\ (\\forall (α,β),\\ α \\simeq β \\to (P\\;α) \\to (P\\;β)) \\to (P\\;PEmpty) \\to (\\forall α [Fintype α], P\\;α) \\to \\forall α [Finite\\; α], P\\;α.$$$
Lean4
/-- An induction principle for finite types, analogous to `Nat.rec`. It effectively says
that every `Fintype` is either `Empty` or `Option α`, up to an `Equiv`. -/
theorem induction_empty_option {P : Type u → Prop} (of_equiv : ∀ {α β}, α ≃ β → P α → P β) (h_empty : P PEmpty)
(h_option : ∀ {α} [Fintype α], P α → P (Option α)) (α : Type u) [Finite α] : P α :=
by
cases nonempty_fintype α
refine Fintype.induction_empty_option ?_ ?_ ?_ α
exacts [fun α β _ => of_equiv, h_empty, @h_option]
