mk_coordChange — Mathlib

English

The pair (b, e1.coordChange e2 b x) equals e2 applied to e1.symm (b, x).

Русский

Пара (b, e1.coordChange e2 b x) равна применению e2 к e1.symm (b, x).

LaTeX

$$$ (b, e_1.coordChange e_2 b x) = e_2 (e_1.toOpenPartialHomeomorph.symm (b, x)) $$$

Lean4

theorem mk_coordChange (e₁ e₂ : Trivialization F proj) {b : B} (h₁ : b ∈ e₁.baseSet) (h₂ : b ∈ e₂.baseSet) (x : F) :
    (b, e₁.coordChange e₂ b x) = e₂ (e₁.toOpenPartialHomeomorph.symm (b, x)) :=
  by
  refine Prod.ext ?_ rfl
  rw [e₂.coe_fst', ← e₁.coe_fst', e₁.apply_symm_apply' h₁]
  · rwa [e₁.proj_symm_apply' h₁]
  · rwa [e₁.proj_symm_apply' h₁]

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