piCongrRight_trans — Mathlib

English

The transitivity of piCongrRight states that composing two coordinatewise AlgEquivs yields the coordinatewise composition of the two families.

Русский

Транзитивность piCongrRight: композиция по координатам двух семейств эквивалентов есть эквивалентность, полученная координатной композицией.

LaTeX

$$$ (\\mathrm{piCongrRight}\\, e_1).trans (\\mathrm{piCongrRight}\\, e_2) = \\mathrm{piCongrRight}\\, (i \\mapsto (e_1(i)).trans (e_2(i))) $$$

Lean4

@[simp]
theorem piCongrRight_trans (e₁ : ∀ i, A₁ i ≃ₐ[R] A₂ i) (e₂ : ∀ i, A₂ i ≃ₐ[R] A₃ i) :
    (piCongrRight e₁).trans (piCongrRight e₂) = piCongrRight fun i ↦ (e₁ i).trans (e₂ i) :=
  rfl

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