linearMapAt — Mathlib

English

A fiberwise linear map equal to e on e.baseSet: e.linearMapAt R b is linear from E_b to F when b ∈ e.baseSet; otherwise it is the zero map.

Русский

Локальное линейное отображение вдоль волокна: если b ∈ e.baseSet, то e.linearMapAt R b линейно отображает E_b в F; иначе нулевое отображение.

LaTeX

$$$ e.linearMapAt R b : E_b \to F \text{ is linear if } b \in e.baseSet; \text{ otherwise } e.linearMapAt R b = 0 $$$

Lean4

/-- A fiberwise linear map equal to `e` on `e.baseSet`. -/
protected def linearMapAt (e : Pretrivialization F (π F E)) [e.IsLinear R] (b : B) : E b →ₗ[R] F :=
  if hb : b ∈ e.baseSet then e.linearEquivAt R b hb else 0

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