Theorems · Theorem · combinatorics

Finite.induction_empty_option

∀ {P : Type u → Prop},
  (∀ {α β : Type u} (a : α ≃ β), P α → P β) →
    P PEmpty.{u + 1} → (∀ {α : Type u} [Fintype α], P α → P (Option α)) → ∀ (α : Type u) [Finite α], 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

10 results in Mathlib

Foundations

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

Assumes

Finite