arrowCongr_apply — Mathlib

English

The arrowCongr Symm preserves symmetry: the symmetric of the composed equivalence equals the composition of the symmetric equivalences.

Русский

Симметрия arrowCongr сохраняется: симметрическая часть композиции эквивалентностей равна композиции симметрических эквивалентностей.

LaTeX

$$$ (e_1.arrowCongr e_2).symm = e_1.symm.arrowCongr e_2.symm $$$

Lean4

@[simp]
theorem arrowCongr_apply (e₁ : E ≃L[𝕜] F) (e₂ : H ≃L[𝕜] G) (f : E →L[𝕜] H) (x : F) :
    e₁.arrowCongr e₂ f x = e₂ (f (e₁.symm x)) :=
  rfl

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