English
For a nonempty FinEnum α, recEmptyOption evaluates to congruence after inserting None at a specific index dependent on card α.
Русский
Для непустого FinEnum α recEmptyOption даёт congruent результат после вставки None в позицию зависящую от card α.
LaTeX
$$$\\text{recEmptyOption\\_pos}(finChoice,congr,empty,option)(α, h) = congr( insertNone(…) , … )$$$
Lean4
/-- 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 `Fin`s 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.
-/
abbrev recOnEmptyOption {P : Type u → Sort v} {α : Type u} (aenum : FinEnum α) (finChoice : (n : ℕ) → Fin (n + 1))
(congr : {α β : Type u} → (_ : FinEnum α) → (_ : FinEnum β) → card β = card α → P α → P β)
(empty : P PEmpty.{u + 1}) (option : {α : Type u} → FinEnum α → P α → P (Option α)) : P α :=
@recEmptyOption P finChoice congr empty option α aenum
