coordChangeL_apply' — Mathlib

English

The pair (b, coordChangeL b) forms the coordinate patch between e and e' on the intersection.

Русский

Пара (b, coordChangeL b) образует координатный участок между e и e' на пересечении.

LaTeX

$$$ mk_coordChangeL R e e' hb y = (b, coordChangeL R e e' b y).$$$

Lean4

/-- A version of `Trivialization.coordChangeL_apply` that fully unfolds `coordChange`. The
right-hand side is ugly, but has good definitional properties for specifically defined
trivializations. -/
theorem coordChangeL_apply' (e e' : Trivialization F (π F E)) [e.IsLinear R] [e'.IsLinear R] {b : B}
    (hb : b ∈ e.baseSet ∩ e'.baseSet) (y : F) :
    coordChangeL R e e' b y = (e' (e.toOpenPartialHomeomorph.symm (b, y))).2 := by
  rw [e.coordChangeL_apply e' hb, e.mk_symm hb.1]

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