coe_continuousLinearEquivAt_eq — Mathlib

English

The forward map and the underlying function of the continuous linear equivalence agree; the forward map equals the underlying evaluation of the equivalence.

Русский

Преобразование вперёд и функция эквивалентности совпадают; прямое отображение совпадает с базовой функцией эквивалентности.

LaTeX

$$$(e.continuousLinearEquivAt(R,b,hb) : E_b \to F) = e.continuousLinearMapAt(R,b)$$$

Lean4

theorem coe_continuousLinearEquivAt_eq (e : Trivialization F (π F E)) [e.IsLinear R] {b : B} (hb : b ∈ e.baseSet) :
    (e.continuousLinearEquivAt R b hb : E b → F) = e.continuousLinearMapAt R b :=
  (e.coe_linearMapAt_of_mem hb).symm

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