English
The target of the σ-twisted trivialization is the product of the base intersection with the universal base space.
Русский
Цель σ-сложной тривиализации равна произведению пересечения базовых множеств и множества-единицы.
LaTeX
$$$\\big( \\operatorname{trivializationAt} (F_1 \\to SL[\\sigma] F_2) (\\lambda x \\mapsto E_1 x \\to SL[\\sigma] E_2 x) x_0 \\big).\\text{target} = ((\\operatorname{trivializationAt} F_1 E_1 x_0).baseSet \\cap (\\operatorname{trivializationAt} F_2 E_2 x_0).baseSet) \\times_s \\operatorname{Set}.univ$,$$
Lean4
@[simp, mfld_simps]
theorem hom_trivializationAt_target (x₀ : B) :
(trivializationAt (F₁ →SL[σ] F₂) (fun x ↦ E₁ x →SL[σ] E₂ x) x₀).target =
((trivializationAt F₁ E₁ x₀).baseSet ∩ (trivializationAt F₂ E₂ x₀).baseSet) ×ˢ Set.univ :=
rfl
