hrecOn₂

Mathlib.GroupTheory.Congruence.Defs

URI: https://scilib.ai/kg/mathlib#Con.hrecOn₂

Lean4

/-- A version of `Quotient.hrecOn₂'` for quotients by `Con`. -/
@[to_additive /-- A version of `Quotient.hrecOn₂'` for quotients by `AddCon`. -/
    ]
protected def hrecOn₂ {cM : Con M} {cN : Con N} {φ : cM.Quotient → cN.Quotient → Sort*} (a : cM.Quotient)
    (b : cN.Quotient) (f : ∀ (x : M) (y : N), φ x y) (h : ∀ x y x' y', cM x x' → cN y y' → f x y ≍ f x' y') : φ a b :=
  Quotient.hrecOn₂' a b f h

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru