hrec_on₂_coe — Mathlib

English

For a,b in M,N and f, h with appropriate coherence, hrec_on_2 evaluated at (a,b) equals f a b.

Русский

Для a∈M, b∈N и функций f, h удовлетворяющих совместимости, значение hrec_on_2 на (a,b) равно f a b.

LaTeX

$$$\\mathrm{Con.hrecOn_2}(\\uparrow a)(\\uparrow b)\\ f\\ h = f\\ a\\ b$$$

Lean4

@[to_additive (attr := simp)]
theorem hrec_on₂_coe {cM : Con M} {cN : Con N} {φ : cM.Quotient → cN.Quotient → Sort*} (a : M) (b : N)
    (f : ∀ (x : M) (y : N), φ x y) (h : ∀ x y x' y', cM x x' → cN y y' → f x y ≍ f x' y') :
    Con.hrecOn₂ (↑a) (↑b) f h = f a b :=
  rfl

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