symm_continuousLinearEquivAt_eq — Mathlib

English

The value of the forward equivalence at a fiber point equals the model fiber coordinate; i.e., applying the equivalence to a fiber element yields its coordinate in F.

Русский

Значение перехода линейной эквивалентности на точке волокна равно координате в целевой фибре.

LaTeX

$$$e.continuousLinearEquivAt(R, b, hb)(x) = (e x).2$ for suitable x in the total space$$

Lean4

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

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