linearMapAt_apply — Mathlib

English

The function e.linearMapAt b, as a linear map, coincides with the evaluation map of the fiber at b when b ∈ e.baseSet.

Русский

Функция e.linearMapAt b, как линейное отображение, совпадает с отображением по волокну в точке b, когда b ∈ e.baseSet.

LaTeX

$$$ e.linearMapAt R b = e.linearEquivAt R b hb .toLinearMap $$$

Lean4

theorem linearMapAt_apply (e : Pretrivialization F (π F E)) [e.IsLinear R] {b : B} (y : E b) :
    e.linearMapAt R b y = if b ∈ e.baseSet then (e ⟨b, y⟩).2 else 0 := by rw [coe_linearMapAt]

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