hrecOn₂'

Mathlib.Data.Quot

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

Lean4

/-- Recursion on two `Quotient` arguments `a` and `b`, result type depends on `⟦a⟧` and `⟦b⟧`. -/
protected def hrecOn₂' {φ : Quotient s₁ → Quotient s₂ → Sort*} (qa : Quotient s₁) (qb : Quotient s₂)
    (f : ∀ a b, φ (Quotient.mk'' a) (Quotient.mk'' b)) (c : ∀ a₁ b₁ a₂ b₂, a₁ ≈ a₂ → b₁ ≈ b₂ → f a₁ b₁ ≍ f a₂ b₂) :
    φ qa qb :=
  Quotient.hrecOn₂ qa qb f c

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

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

Разделы

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

Аффилиация

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