coe_linearMapAt — Mathlib

English

A fiberwise linear map is defined to be e.linearMapAt; if the base point is not in the base set, the map is zero.

Русский

Локальное линейное отображение задано как e.linearMapAt; если базовая точка не в базовом множестве, отображение равно 0.

LaTeX

$$e.linearMapAt R b = 0 if b ∉ e.baseSet; otherwise e.linearMapAt R b = e.linearEquivAt R b hb toLinearMap$$

Lean4

theorem coe_linearMapAt (e : Pretrivialization F (π F E)) [e.IsLinear R] (b : B) :
    ⇑(e.linearMapAt R b) = fun y => if b ∈ e.baseSet then (e ⟨b, y⟩).2 else 0 :=
  by
  rw [Pretrivialization.linearMapAt]
  split_ifs <;> rfl

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