English
The forward map of the product trivialization is continuously defined on the domain where both base trivializations are valid.
Русский
Отображение вперед для произведения тривиализации непрерывно на области определения, где обе базовые тривиализации допустимы.
LaTeX
$$$\mathrm{ContinuousOn}(\mathrm{Prod.toFun'}(e_1,e_2),\ \pi^{-1}(e_1.baseSet \cap e_2.baseSet))$$$
Lean4
theorem continuous_to_fun : ContinuousOn (Prod.toFun' e₁ e₂) (π (F₁ × F₂)(E₁ ×ᵇ E₂) ⁻¹' (e₁.baseSet ∩ e₂.baseSet)) :=
by
let f₁ : TotalSpace (F₁ × F₂) (E₁ ×ᵇ E₂) → TotalSpace F₁ E₁ × TotalSpace F₂ E₂ := fun p ↦
((⟨p.1, p.2.1⟩ : TotalSpace F₁ E₁), (⟨p.1, p.2.2⟩ : TotalSpace F₂ E₂))
let f₂ : TotalSpace F₁ E₁ × TotalSpace F₂ E₂ → (B × F₁) × B × F₂ := fun p ↦ ⟨e₁ p.1, e₂ p.2⟩
let f₃ : (B × F₁) × B × F₂ → B × F₁ × F₂ := fun p ↦ ⟨p.1.1, p.1.2, p.2.2⟩
have hf₁ : Continuous f₁ := (Prod.isInducing_diag F₁ E₁ F₂ E₂).continuous
have hf₂ : ContinuousOn f₂ (e₁.source ×ˢ e₂.source) :=
e₁.toOpenPartialHomeomorph.continuousOn.prodMap e₂.toOpenPartialHomeomorph.continuousOn
have hf₃ : Continuous f₃ := by fun_prop
refine ((hf₃.comp_continuousOn hf₂).comp hf₁.continuousOn ?_).congr ?_
· rw [e₁.source_eq, e₂.source_eq]
exact mapsTo_preimage _ _
rintro ⟨b, v₁, v₂⟩ ⟨hb₁, _⟩
simp only [f₁, f₂, f₃, Prod.toFun', Prod.mk_inj, Function.comp_apply, and_true]
rw [e₁.coe_fst]
rw [e₁.source_eq, mem_preimage]
exact hb₁
