Theorems · Theorem · combinatorics

FinEnum.recEmptyOption_of_card_eq_zero

∀ {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 : FinEnum.card α = 0) (x : FinEnum PEmpty.{u + 1}),
  FinEnum.recEmptyOption finChoice (fun {α β} => congr) empty (fun {α} => option) α = congr x inst ⋯ empty

For an empty type, the recursion principle evaluates to whatever congr makes of the base case.

Defined in

Mathlib.Data.FinEnum.Option

Cited by

0 results in Mathlib

Foundations

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

Assumes

FinEnum