chartAt — Mathlib

English

The preferred chart at a point x in a charted space M is the chart At x.

Русский

Предпочтительная диаграмма в точке x пространства charted space M — это chartAt x.

LaTeX

$$$chartAt(H,x) \\text{ is the chart at } x$$$

Lean4

/-- The preferred chart at a point `x` in a charted space `M`. -/
abbrev chartAt (H : Type*) [TopologicalSpace H] {M : Type*} [TopologicalSpace M] [ChartedSpace H M] (x : M) :
    OpenPartialHomeomorph M H :=
  ChartedSpace.chartAt x

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