achart — Mathlib

English

An achart is the chart at x together with its membership in the atlas.

Русский

Achart — это chartAt(H,x) вместе с принадлежностью к атласу.

LaTeX

$$$\\text{achart}(H,x) = \\langle \\text{chartAt}(H,x), \\text{chart\_mem\_atlas}(H,x) \\rangle$$$

Lean4

/-- `achart H x` is the chart at `x`, considered as an element of the atlas.
Especially useful for working with `BasicContMDiffVectorBundleCore`. -/
def achart (x : M) : atlas H M :=
  ⟨chartAt H x, chart_mem_atlas H x⟩

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