Theorems · Theorem · combinatorics

Fintype.induction_empty_option

∀ {P : (α : Type u) → [Fintype α] → Prop},
  (∀ (α β : Type u) [inst : Fintype β] (e : α ≃ β), P α → P β) →
    P PEmpty.{u + 1} →
      (∀ (α : Type u) [inst : Fintype α], P α → P (Option α)) → ∀ (α : Type u) [h_fintype : Fintype α], P α

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.

Defined in

Mathlib.Data.Fintype.Option

Cited by

6 results in Mathlib

Foundations

Depth 69 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Fintype