equivCongr_refl_left — Mathlib

English

The left-hand side of the equivalence-congruence with a reflexive equivalence is the same as the right-hand side composed with the left and the right equivalences.

Русский

Левая часть равенства-equiv-congr с тождественным отображением совпадает с правой частью, составленной слева и справа.

LaTeX

$$$(\\text{refl } α).equivCongr bg e = e.trans bg$$$

Lean4

@[simp]
theorem equivCongr_refl_left {α β γ} (bg : β ≃ γ) (e : α ≃ β) : (Equiv.refl α).equivCongr bg e = e.trans bg :=
  rfl

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