Mathlib Map

Theorems · Definition · order theory

Quotient.mkRelHom

{α : Type u_1} →
  {x : Setoid α} →
    {r : α → α → Prop} → (H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂) → r →r Quotient.lift₂ r H

Quotient.mk as a relation homomorphism between the relation and the lift of a relation.

Defined in
Mathlib.Order.RelIso.Basic
Cited by
3 results in Mathlib
Foundations
Depth 7 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

wellFounded_lift₂_iff · cited by 5wellFounded_lift₂_iffacc_lift₂_iff · cited by 3acc_lift₂_iffQuotient.mkRelHom_apply · cited by 0Quotient.mkRelHom_applyRelHom · cited by 49RelHomQuotient.mkRelHomCITED BYCITES

Cites1

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • RelHomstatement · cited by 49

Cited by3

Results whose statement or proof uses this declaration.