linearMapAt_symmₗ — Mathlib

English

If hb is a membership in the base set, then e.linearMapAt R b equals e.linearEquivAt R b hb as linear maps.

Русский

Если hb принадлежит базовому множеству, то e.linearMapAt R b совпадает с e.linearEquivAt R b hb как линейные отображения.

LaTeX

$$$\forall hb\in e.baseSet,\; e.linearMapAt R b = e.linearEquivAt R b hb.$$$

Lean4

theorem linearMapAt_symmₗ (e : Trivialization F (π F E)) [e.IsLinear R] {b : B} (hb : b ∈ e.baseSet) (y : F) :
    e.linearMapAt R b (e.symmₗ R b y) = y :=
  e.toPretrivialization.linearMapAt_symmₗ hb y

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