Theorems · Theorem · combinatorics

FinEnum.recEmptyOption_of_card_pos

∀ {P : Type u → Sort v} (finChoice : (n : ℕ) → Fin (n + 1))
  (congr : {α β : Type u} → (x : FinEnum α) → (x_1 : FinEnum β) → FinEnum.card β = FinEnum.card α → P α → P β)
  (empty : P PEmpty.{u + 1}) (option : {α : Type u} → FinEnum α → P α → P (Option α)) (α : Type u) [inst : FinEnum α]
  (h : 0 < FinEnum.card α),
  FinEnum.recEmptyOption finChoice (fun {α β} => congr) empty (fun {α} => option) α =
    congr (FinEnum.insertNone (ULift.{u, 0} (Fin (FinEnum.card α - 1))) ↑↑(finChoice (FinEnum.card α - 1))) inst ⋯
      (option ULift.instFinEnum
        (FinEnum.recEmptyOption finChoice (fun {α β} => congr) empty (fun {α} => option)
          (ULift.{u, 0} (Fin (FinEnum.card α - 1)))))

For a type with positive card, the recursion principle evaluates to whatever congr makes of the step result, where Option.none has been inserted into the (finChoice (card α - 1))th rank of the enumeration.

Defined in

Mathlib.Data.FinEnum.Option

Cited by

0 results in Mathlib

Foundations

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

Assumes

FinEnum