left_inv — Mathlib

English

On the base-expanded domain, applying toFun' after invFun' returns the original element.

Русский

На области домена в базе, применение toFun' после invFun' возвращает исходный элемент.

LaTeX

$$$\forall x \in (e_1.baseSet \cap e_2.baseSet) \times \mathrm{univ},\ \mathrm{toFun'}(e_1,e_2)(\mathrm{invFun'}(e_1,e_2)(x)) = x$$$

Lean4

theorem left_inv {x : TotalSpace (F₁ × F₂) (E₁ ×ᵇ E₂)} (h : x ∈ π (F₁ × F₂)(E₁ ×ᵇ E₂) ⁻¹' (e₁.baseSet ∩ e₂.baseSet)) :
    Prod.invFun' e₁ e₂ (Prod.toFun' e₁ e₂ x) = x :=
  by
  obtain ⟨x, v₁, v₂⟩ := x
  obtain ⟨h₁ : x ∈ e₁.baseSet, h₂ : x ∈ e₂.baseSet⟩ := h
  simp only [Prod.toFun', Prod.invFun', symm_apply_apply_mk, h₁, h₂]

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