withTopCongr_trans — Mathlib

English

The lifting respects composition: withTopCongr(e1.trans e2) = (withTopCongr e1).trans (withTopCongr e2).

Русский

Переносимость сохраняет композицию: withTopCongr(e1.trans e2) = (withTopCongr e1).trans (withTopCongr e2).

LaTeX

$$$\mathrm{withTopCongr}(e_1 \;\mathrm{trans}\; e_2) = (\mathrm{withTopCongr}(e_1)).\mathrm{trans}(\mathrm{withTopCongr}(e_2))$$$

Lean4

@[simp]
theorem withTopCongr_trans (e₁ : α ≃ β) (e₂ : β ≃ γ) :
    withTopCongr (e₁.trans e₂) = (withTopCongr e₁).trans (withTopCongr e₂) :=
  by
  ext x
  simp

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