finRecOn — Mathlib

English

A simp lemma for finRecOn showing it reduces to f a on mk.

Русский

Лемма упрощения для finRecOn, показывающая сведение к f a на mk.

LaTeX

$$$\\operatorname{finHRecOn}(\\llbracket a \\rrbracket) = \\lambda f, _. f a$$$

Lean4

/-- Recursion principle for quotients indexed by a finite type. -/
@[elab_as_elim]
def finRecOn {C : (∀ i, Quotient (S i)) → Sort*} (q : ∀ i, Quotient (S i)) (f : ∀ a : ∀ i, α i, C (⟦a ·⟧))
    (h : ∀ (a b : ∀ i, α i) (h : ∀ i, a i ≈ b i), Eq.ndrec (f a) (funext fun i ↦ Quotient.sound (h i)) = f b) : C q :=
  finHRecOn q f (eqRec_heq_iff_heq.mp <| heq_of_eq <| h · · ·)

Похожие утверждения