trivializationAt_source — Mathlib

English

The source of the trivialization equals the preimage of the chart source under the projection.

Русский

Источник тривиализации равен прообразу исходной области чарта под проекцией.

LaTeX

$$$$ (trivializationAt E (TangentSpace I) x).source = \pi E(TangentSpace I)^{-1} (chartAt H x).source $$$$

Lean4

@[simp, mfld_simps]
theorem trivializationAt_source (x : M) :
    (trivializationAt E (TangentSpace I) x).source = π E(TangentSpace I) ⁻¹' (chartAt H x).source :=
  rfl

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