English
The continuous linear equivalence on the product trivialization is the product-congruence of the piecewise linear equivalences on each factor.
Русский
Непрерывное линейное эквивалентное отображение на произведённой тривиализации равняется произведению эквивалентностей по каждому фактору.
LaTeX
$$$ (e_1 \\!\\cdot\\! e_2).continuousLinearEquivAt 𝕜 x hx = (e_1.continuousLinearEquivAt 𝕜 x hx.1).prodCongr (e_2.continuousLinearEquivAt 𝕜 x hx.2) $$$
Lean4
@[simp]
theorem continuousLinearEquivAt_prod {e₁ : Trivialization F₁ (π F₁ E₁)} {e₂ : Trivialization F₂ (π F₂ E₂)}
[e₁.IsLinear 𝕜] [e₂.IsLinear 𝕜] {x : B} (hx : x ∈ (e₁.prod e₂).baseSet) :
(e₁.prod e₂).continuousLinearEquivAt 𝕜 x hx =
(e₁.continuousLinearEquivAt 𝕜 x hx.1).prodCongr (e₂.continuousLinearEquivAt 𝕜 x hx.2) :=
by
ext v : 2
obtain ⟨v₁, v₂⟩ := v
rw [(e₁.prod e₂).continuousLinearEquivAt_apply 𝕜, Trivialization.prod]
exact (congr_arg Prod.snd (prod_apply' 𝕜 hx.1 hx.2 v₁ v₂) :)
