coordChange_coordChange — Mathlib

English

On the base set, the coordinate change equals the identity map.

Русский

На базовом множестве переход координат равен тождественному отображению.

LaTeX

$$$e.coordChange e b = \\mathrm{id}$ on e.baseSet$$

Lean4

theorem coordChange_coordChange (e₁ e₂ e₃ : Trivialization F proj) {b : B} (h₁ : b ∈ e₁.baseSet) (h₂ : b ∈ e₂.baseSet)
    (x : F) : e₂.coordChange e₃ b (e₁.coordChange e₂ b x) = e₁.coordChange e₃ b x :=
  by
  rw [coordChange, e₁.mk_coordChange _ h₁ h₂, ← e₂.coe_coe, e₂.left_inv, coordChange]
  rwa [e₂.mem_source, e₁.proj_symm_apply' h₁]

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