English
An induction principle for finite types: every finite type is either Empty or Option α, up to Equivalence.
Русский
Индукционная схема по конечным типам: любой конечный тип эквивалентен Empty или Option α.
LaTeX
$$@[elab_as_elim] induction_empty_option {P : ∀ (α : Type u) [Fintype α], Prop} (of_equiv : ∀ (α β) [Fintype β] (e : α ≃ β), @P α (@Fintype.ofEquiv α β ‹_› e.symm) → @P β ‹_›) (h_empty : P PEmpty) (h_option : ∀ (α) [Fintype α], P α → P (Option α)) (α : Type u) [h_fintype : Fintype α] : 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`. -/
@[elab_as_elim]
theorem induction_empty_option {P : ∀ (α : Type u) [Fintype α], Prop}
(of_equiv : ∀ (α β) [Fintype β] (e : α ≃ β), @P α (@Fintype.ofEquiv α β ‹_› e.symm) → @P β ‹_›) (h_empty : P PEmpty)
(h_option : ∀ (α) [Fintype α], P α → P (Option α)) (α : Type u) [h_fintype : Fintype α] : P α :=
by
obtain ⟨p⟩ :=
let f_empty := fun i => by convert h_empty
let h_option :
∀ {α : Type u} [Fintype α] [DecidableEq α], (∀ (h : Fintype α), P α) → ∀ (h : Fintype (Option α)), P (Option α) :=
by
rintro α hα - Pα hα'
convert h_option α (Pα _)
@truncRecEmptyOption (fun α => ∀ h, @P α h) (@fun α β e hα hβ => @of_equiv α β hβ e (hα _)) f_empty h_option α _
(Classical.decEq α)
exact
p
_
-- ·
