linearMapAt_def_of_mem — Mathlib

English

The LinearMapAt is the linear map from E_b to F given by y ↦ the second component of e ⟨b,y⟩, when b ∈ baseSet; otherwise defined as 0.

Русский

LinearMapAt задает линейное отображение из E_b в F: y ↦ вторая компонента пары e ⟨b,y⟩, если b в базовом множестве; иначе 0.

LaTeX

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

Lean4

theorem linearMapAt_def_of_mem (e : Pretrivialization F (π F E)) [e.IsLinear R] {b : B} (hb : b ∈ e.baseSet) :
    e.linearMapAt R b = e.linearEquivAt R b hb :=
  dif_pos hb

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