withBotCongr_trans — Mathlib

English

The withBotCongr construction is compatible with composition of order isomorphisms: the withBotCongr of a composite equals the composite of the withBotCongrs.

Русский

Согласование withBotCongr совместимо с композицией изоморфизмов: withBotCongr от композиции равен композиции withBotCongr.

LaTeX

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

Lean4

@[simp]
theorem withBotCongr_trans (e₁ : α ≃o β) (e₂ : β ≃o γ) :
    (e₁.trans e₂).withBotCongr = e₁.withBotCongr.trans e₂.withBotCongr :=
  RelIso.toEquiv_injective <| e₁.toEquiv.withBotCongr_trans e₂.toEquiv

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