withBotCongr_trans — Mathlib

English

Congruence respects composition: withBotCongr (e1.trans e2) = (withBotCongr e1).trans (withBotCongr e2).

Русский

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

LaTeX

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

Lean4

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

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