continuousLinearMap_apply — Mathlib

English

The base set of the product continuousLinearMap equals the intersection of the base sets and the example demonstrates the end-to-end continuity of the coordinate changes on the atlas.

Русский

База множества произведённого continuousLinearMap равна пересечению базовых множеств и пример демонстрирует непрерывность координатного изменения в атласе.

LaTeX

$$$ (e_1.continuousLinearMap σ e_2).baseSet = e_1.baseSet \\cap e_2.baseSet $$$

Lean4

theorem continuousLinearMap_apply (p : TotalSpace (F₁ →SL[σ] F₂) (fun x ↦ E₁ x →SL[σ] E₂ x)) :
    e₁.continuousLinearMap σ e₂ p =
      ⟨p.1,
        (e₂.continuousLinearMapAt 𝕜₂ p.1 : _ →L[𝕜₂] _).comp
          (p.2.comp (e₁.symmL 𝕜₁ p.1 : F₁ →L[𝕜₁] E₁ p.1) : F₁ →SL[σ] E₂ p.1)⟩ :=
  rfl

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