English
The fiberwise linear inverse symmₗ is the inverse of linearMapAt on fibers.
Русский
Линейное обратное вдоль волокна symmₗ является обратным к линейному отображению на волокнах.
LaTeX
$$$ e.symm_\ell R b (e.linearMapAt R b y) = y$, для all y ∈ E_b.$$
Lean4
/-- A coordinate change function between two trivializations, as a continuous linear equivalence.
Defined to be the identity when `b` does not lie in the base set of both trivializations. -/
def coordChangeL (e e' : Trivialization F (π F E)) [e.IsLinear R] [e'.IsLinear R] (b : B) : F ≃L[R] F :=
{ toLinearEquiv :=
if hb : b ∈ e.baseSet ∩ e'.baseSet then (e.linearEquivAt R b (hb.1 :)).symm.trans (e'.linearEquivAt R b hb.2)
else LinearEquiv.refl R F
continuous_toFun := by
by_cases hb : b ∈ e.baseSet ∩ e'.baseSet
· rw [dif_pos hb]
refine (e'.continuousOn.comp_continuous ?_ ?_).snd
· exact e.continuousOn_symm.comp_continuous (Continuous.prodMk_right b) fun y => mk_mem_prod hb.1 (mem_univ y)
· exact fun y => e'.mem_source.mpr hb.2
· rw [dif_neg hb]
exact continuous_id
continuous_invFun := by
by_cases hb : b ∈ e.baseSet ∩ e'.baseSet
· rw [dif_pos hb]
refine (e.continuousOn.comp_continuous ?_ ?_).snd
· exact e'.continuousOn_symm.comp_continuous (Continuous.prodMk_right b) fun y => mk_mem_prod hb.2 (mem_univ y)
exact fun y => e.mem_source.mpr hb.1
· rw [dif_neg hb]
exact continuous_id }
