Theorems · Theorem · combinatorics

FinEnum.recEmptyOption.eq_def

∀ {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 α],
  FinEnum.recEmptyOption finChoice congr empty option α =
    match cardeq : FinEnum.card α with
    | 0 => congr FinEnum.pempty inst cardeq empty
    | n.succ =>
      let fN := ULift.instFinEnum;
      have this := ⋯;
      congr (FinEnum.insertNone (ULift.{u, 0} (Fin n)) ↑↑(finChoice n)) inst ⋯
        (option fN
          (FinEnum.recEmptyOption finChoice (fun {α β} => congr) empty (fun {α} => option) (ULift.{u, 0} (Fin n))))

Defined in

Mathlib.Data.FinEnum.Option

Cited by

2 results in Mathlib

Foundations

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

Assumes

FinEnum