continuous_inv_fun — Mathlib

English

The forward map of the product trivialization is continuous on the open base-set intersection.

Русский

Отображение вперед тривиализации на открытом пересечении базовых множеств непрерывно.

LaTeX

$$$\mathrm{ContinuousOn}(\mathrm{Prod.toFun'}(e_1,e_2),\ e_1.baseSet \cap e_2.baseSet)$$$

Lean4

theorem continuous_inv_fun : ContinuousOn (Prod.invFun' e₁ e₂) ((e₁.baseSet ∩ e₂.baseSet) ×ˢ univ) :=
  by
  rw [(Prod.isInducing_diag F₁ E₁ F₂ E₂).continuousOn_iff]
  have H₁ : Continuous fun p : B × F₁ × F₂ ↦ ((p.1, p.2.1), (p.1, p.2.2)) := by fun_prop
  refine (e₁.continuousOn_symm.prodMap e₂.continuousOn_symm).comp H₁.continuousOn ?_
  exact fun x h ↦ ⟨⟨h.1.1, mem_univ _⟩, ⟨h.1.2, mem_univ _⟩⟩

Похожие утверждения