coe_linearMapAt_of_mem — Mathlib

English

For b ∈ e.baseSet and any y ∈ E_b, the value of e.linearMapAt R b y equals the second component of e ⟨b,y⟩.

Русский

Для b ∈ e.baseSet и любого y ∈ E_b значение e.linearMapAt R b y равно второй компоненте пары e ⟨b,y⟩.

LaTeX

$$$ e.linearMapAt R b \; y = (e ⟨b,y⟩).2 \quad ( \text{when } b ∈ e.baseSet) $$$

Lean4

theorem coe_linearMapAt_of_mem (e : Pretrivialization F (π F E)) [e.IsLinear R] {b : B} (hb : b ∈ e.baseSet) :
    ⇑(e.linearMapAt R b) = fun y => (e ⟨b, y⟩).2 := by simp_rw [coe_linearMapAt, if_pos hb]

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