continuousLinearMapAt_symmL — Mathlib

English

The backward map composed with the forward map yields the identity on the fiber: e.symmL(R,b) ∘ e.continuousLinearMapAt(R,b) = id_{E_b} for b in base.

Русский

Обратное отображение в композиции с прямым отображением даёт тождество на волокне: e.symmL(R,b) ∘ e.continuousLinearMapAt(R,b) = id_{E_b} при b в base.

LaTeX

$$$(e.symmL(R,b) \circ e.continuousLinearMapAt(R,b)) = \mathrm{id}_{E_b}$ для всех $b$ в базовом множестве$$

Lean4

theorem continuousLinearMapAt_symmL (e : Trivialization F (π F E)) [e.IsLinear R] {b : B} (hb : b ∈ e.baseSet) (y : F) :
    e.continuousLinearMapAt R b (e.symmL R b y) = y :=
  e.linearMapAt_symmₗ hb y

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