Theorems · Definition · combinatorics

FinEnum.recOnEmptyOption

{P : Type u → Sort v} →
  {α : Type u} →
    FinEnum α →
      ((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 α)) → P α

A recursor principle for finite-and-enumerable types, analogous to Nat.recOn. 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.

Defined in

Mathlib.Data.FinEnum.Option

Cited by

0 results in Mathlib

Foundations

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