coe_linearMapAt_of_mem — Mathlib

English

Between two linear trivializations, the coordinate change at b is a linear equivalence and provides a smooth patching on their intersection.

Русский

Между двумя линейными тривиализациями координаты при b образуют линейное эквивалентное отображение и дают гладкое стыковочное отображение на пересечении.

LaTeX

$$$ coordChangeL R e e' b : F \cong_R F$ is a continuous linear equivalence.$$

Lean4

theorem coe_linearMapAt_of_mem (e : Trivialization F (π F E)) [e.IsLinear R] {b : B} (hb : b ∈ e.baseSet) :
    ⇑(e.linearMapAt R b) = fun y => (e ⟨b, y⟩).2 := by simp_rw [coe_linearMapAt, if_pos hb]

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