English
Transport a RelHom across a pair of RelIso's by pre- and post-composition, giving an equivalence between RelHoms.
Русский
Перевозим RelHom через пару RelIso путём лево- и право-композиции, получая эквивалентность между RelHom.
LaTeX
$$$$ \text{relHomCongr} \{\alpha_1,\beta_1,\alpha_2,\beta_2\} (e_1,e_2) : (r_1 \to_r s_1) \simeq (r_2 \to_r s_2). $$$$
Lean4
/-- Transport a `RelHom` across a pair of `RelIso`s, by pre- and post-composition.
This is `Equiv.arrowCongr` for `RelHom`. -/
@[simps]
def relHomCongr {α₁ β₁ α₂ β₂} {r₁ : α₁ → α₁ → Prop} {s₁ : β₁ → β₁ → Prop} {r₂ : α₂ → α₂ → Prop} {s₂ : β₂ → β₂ → Prop}
(e₁ : r₁ ≃r r₂) (e₂ : s₁ ≃r s₂) : (r₁ →r s₁) ≃ (r₂ →r s₂)
where
toFun f₁ := e₂.toRelEmbedding.toRelHom.comp <| f₁.comp e₁.symm.toRelEmbedding.toRelHom
invFun f₂ := e₂.symm.toRelEmbedding.toRelHom.comp <| f₂.comp e₁.toRelEmbedding.toRelHom
left_inv f₁ := by ext; simp
right_inv f₂ := by ext; simp
