continuousLinearMap_symm_apply — Mathlib

English

The total space topology for the bundle of continuous linear maps is defined by the totalSpaceTopology from the underlying vector prebundle.

Русский

Топология полного пространства для расслоения непрерывных линейных отображений задаётся через topology of total space из базового векторного претривиализа.

LaTeX

$$$\\text{topologicalSpaceTotalSpace } = \\text{vectorPrebundle}.totalSpaceTopology$$$

Lean4

theorem continuousLinearMap_symm_apply (p : B × (F₁ →SL[σ] F₂)) :
    (continuousLinearMap σ e₁ e₂).toPartialEquiv.symm p =
      ⟨p.1, .comp (e₂.symmL 𝕜₂ p.1) (p.2.comp (e₁.continuousLinearMapAt 𝕜₁ p.1))⟩ :=
  rfl

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