finHRecOn_mk — Mathlib

English

A simp lemma for finHRecOn giving f a when q is mk of a.

Русский

Лемма упрощения для finHRecOn, дающая f a, когда q = mk a.

LaTeX

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

Lean4

@[simp]
theorem finHRecOn_mk {C : (∀ i, Quotient (S i)) → Sort*} (a : ∀ i, α i) : finHRecOn (C := C) (⟦a ·⟧) = fun f _ ↦ f a :=
  by
  ext f h
  refine eq_of_heq ((eqRec_heq _ _).trans ?_)
  rw [finChoice_eq]
  rfl

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