arrowCongr — Mathlib

English

Explicit evaluation of arrowCongr: arrowCongr applied to f yields the map x ↦ e2(f(e1^{-1} x)).

Русский

Явное выражение arrowCongr: применяя к f получаем отображение x ↦ e2(f(e1^{-1} x)).

LaTeX

$$$ (e_1.arrowCongr e_2) f x = e_2 \\big( f (e_1^{-1} x) \\big) $$$

Lean4

/-- A pair of continuous linear equivalences generates a continuous linear equivalence between
the spaces of continuous linear maps. -/
def arrowCongr (e₁ : E ≃L[𝕜] F) (e₂ : H ≃L[𝕜] G) : (E →L[𝕜] H) ≃L[𝕜] F →L[𝕜] G :=
  e₁.arrowCongrSL e₂

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