English
The map continuousLinearMapCoordChange is continuous on the intersection of base sets and describes the coordinate change of the induced pretrivializations.
Русский
Координатное изменение continuousLinearMapCoordChange непрерывно на пересечении базовых множеств и задаёт координатное изменение соответствующих предтривиализаций.
LaTeX
$$$ ContinuousOn (continuousLinearMapCoordChange σ e_1 e_1' e_2 e_2') (e_1.baseSet \\cap e_2.baseSet \\cap (e_1'.baseSet \\cap e_2'.baseSet)) $$$
Lean4
instance isLinear [∀ x, ContinuousAdd (E₂ x)] [∀ x, ContinuousSMul 𝕜₂ (E₂ x)] :
(Pretrivialization.continuousLinearMap σ e₁ e₂).IsLinear 𝕜₂ where
linear x
_ :=
{ map_add := fun L L' ↦
show (e₂.continuousLinearMapAt 𝕜₂ x).comp ((L + L').comp (e₁.symmL 𝕜₁ x)) = _
by
simp_rw [add_comp, comp_add]
rfl
map_smul := fun c L ↦
show (e₂.continuousLinearMapAt 𝕜₂ x).comp ((c • L).comp (e₁.symmL 𝕜₁ x)) = _
by
simp_rw [smul_comp, comp_smulₛₗ, RingHom.id_apply]
rfl }
