Theorems · Definition · combinatorics

FinEnum.recEmptyOption

{P : Type u → Sort v} →
  ((n : ℕ) → Fin (n + 1)) →
    ({α β : Type u} → (x : FinEnum α) → (x_1 : FinEnum β) → FinEnum.card β = FinEnum.card α → P α → P β) →
      P PEmpty.{u + 1} → ({α : Type u} → FinEnum α → P α → P (Option α)) → (α : Type u) → [FinEnum α] → P α

A recursor principle for finite-and-enumerable types, analogous to Nat.rec. It effectively says that every FinEnum is either Empty or Option α, up to an Equiv mediated by Fins of equal cardinality. In contrast to the Fintype case, data can be transported along such an Equiv. Also, since order matters, the choice of element that gets replaced by Option.none has to be provided for every step. Since every FinEnum instance implies a Fintype instance and Prop is squashed already, Fintype.induction_empty_option can be used if a Prop needs to be constructed. Cf. Data.Fintype.Option

Defined in

Mathlib.Data.FinEnum.Option

Cited by

3 results in Mathlib

Foundations

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

Assumes

FinEnum