invFun' — Mathlib

English

On the domain of the product trivialization, applying invFun' after toFun' recovers the original element.

Русский

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

LaTeX

$$$\forall x \in \pi^{-1}'(e_1.baseSet \cap e_2.baseSet),\ Prod.invFun'(e_1,e_2)(Prod.toFun'(e_1,e_2)(x)) = x$$$

Lean4

/-- Given trivializations `e₁`, `e₂` for fiber bundles `E₁`, `E₂` over a base `B`, the inverse
function for the construction `Trivialization.prod`, the induced
trivialization for the fiberwise product of `E₁` and `E₂`. -/
noncomputable def invFun' (p : B × F₁ × F₂) : TotalSpace (F₁ × F₂) (E₁ ×ᵇ E₂) :=
  ⟨p.1, e₁.symm p.1 p.2.1, e₂.symm p.1 p.2.2⟩

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