coordChange_apply_snd — Mathlib

English

The composition of two fiber coordinate changes is associative: e2.coordChange e3 b (e1.coordChange e2 b x) = e1.coordChange e3 b x.

Русский

Объединение двух переходов координат в волокне ассоциативно: e2.coordChange e3 b (e1.coordChange e2 b x) = e1.coordChange e3 b x.

LaTeX

$$$e_2.coordChange e_3 b (e_1.coordChange e_2 b x) = e_1.coordChange e_3 b x$$$

Lean4

theorem coordChange_apply_snd (e₁ e₂ : Trivialization F proj) {p : Z} (h : proj p ∈ e₁.baseSet) :
    e₁.coordChange e₂ (proj p) (e₁ p).snd = (e₂ p).snd := by rw [coordChange, e₁.symm_apply_mk_proj (e₁.mem_source.2 h)]

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