right_inv — Mathlib

English

The inverse map of the product trivialization is continuous on its base domain.

Русский

Обратная карта произведения тривиализации непрерывна на своей области определения.

LaTeX

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

Lean4

theorem right_inv {x : B × F₁ × F₂} (h : x ∈ (e₁.baseSet ∩ e₂.baseSet) ×ˢ (univ : Set (F₁ × F₂))) :
    Prod.toFun' e₁ e₂ (Prod.invFun' e₁ e₂ x) = x :=
  by
  obtain ⟨x, w₁, w₂⟩ := x
  obtain ⟨⟨h₁ : x ∈ e₁.baseSet, h₂ : x ∈ e₂.baseSet⟩, -⟩ := h
  simp only [Prod.toFun', Prod.invFun', apply_mk_symm, h₁, h₂]

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