prod_symm_apply — Mathlib

English

The inverse of the product trivialization applied to a basic tuple yields the expected triple with base and fiber coordinates.

Русский

Обратное к тривиализации произведения, примененное к базовой троице, дает ожидаемую тройку с базовой и фибровой координатами.

LaTeX

$$$(\mathrm{prod}(e_1,e_2).\mathrm{toPartialEquiv}.\mathrm{symm})(x,w_1,w_2) = \langle x, e_1.x(x) w_1, e_2.x(x) w_2\rangle$$$

Lean4

theorem prod_symm_apply (x : B) (w₁ : F₁) (w₂ : F₂) :
    (prod e₁ e₂).toPartialEquiv.symm (x, w₁, w₂) = ⟨x, e₁.symm x w₁, e₂.symm x w₂⟩ :=
  rfl

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