coordChangeHomeomorph_coe — Mathlib

English

The underlying function of the coordinate-change homeomorph equals the fiber coordinate change function.

Русский

Функция, лежащая в основе перехода координат, равна переходу координат по волокну.

LaTeX

$$$ (e_1.coordChangeHomeomorph e_2 h_1 h_2).toFun = e_1.coordChange e_2 b $$$

Lean4

@[simp]
theorem coordChangeHomeomorph_coe (e₁ e₂ : Trivialization F proj) {b : B} (h₁ : b ∈ e₁.baseSet) (h₂ : b ∈ e₂.baseSet) :
    ⇑(e₁.coordChangeHomeomorph e₂ h₁ h₂) = e₁.coordChange e₂ b :=
  rfl

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