Theorems · Theorem · order theory

RelIso.relHomCongr_apply

∀ {α₁ : Type u_5} {β₁ : Type u_6} {α₂ : Type u_7} {β₂ : Type u_8} {r₁ : α₁ → α₁ → Prop} {s₁ : β₁ → β₁ → Prop}
  {r₂ : α₂ → α₂ → Prop} {s₂ : β₂ → β₂ → Prop} (e₁ : r₁ ≃r r₂) (e₂ : s₁ ≃r s₂) (f₁ : r₁ →r s₁),
  (e₁.relHomCongr e₂) f₁ = e₂.toRelEmbedding.toRelHom.comp (f₁.comp e₁.symm.toRelEmbedding.toRelHom)

Defined in

Mathlib.Order.RelIso.Basic

Cited by

0 results in Mathlib

Foundations

Depth 27 from the axioms · uses propext, Quot.sound