equivCongr_trans — Mathlib

English

Equivalences respect composition: (ab ≃ bc) and (de ≃ ε) satisfy the compatibility transitivity: (ab.equivCongr de).trans (bc.equivCongr ef) = (ab.trans bc).equivCongr (de.trans ef).

Русский

Эквивалентности сохраняют композицию: выполняется тождество совместимости между переводами через равенства.

LaTeX

$$$((ab\\ equivCongr de).trans (bc.equivCongr ef)) = ((ab.trans bc).equivCongr (de.trans ef))$$$

Lean4

@[simp]
theorem equivCongr_trans {δ ε ζ} (ab : α ≃ β) (de : δ ≃ ε) (bc : β ≃ γ) (ef : ε ≃ ζ) :
    (ab.equivCongr de).trans (bc.equivCongr ef) = (ab.trans bc).equivCongr (de.trans ef) := by grind

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