localTrivAt_snd — Mathlib

English

The source of the local trivialization is open, and the coordinate-change maps between charts are continuous on their domains.

Русский

Источник локальной тривиализации открыто, а переходы координат между картами непрерывны на своих областях.

LaTeX

$$$\\text{open_source'}: \\text{IsOpen}(\\mathrm{source}(\\mathcal{L}_i)) \ \&\\ \\text{continuousOn_toFun}$ (and analogous properties).$$

Lean4

theorem localTrivAt_snd (b : B) (p) : (Z.localTrivAt b p).2 = Z.coordChange (Z.indexAt p.1) (Z.indexAt b) p.1 p.2 :=
  rfl

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