chartedSpaceSelf_atlas — Mathlib

English

There is a canonical charted space structure on a space modeled on itself via the identity atlas.

Русский

Для пространства, моделируемого самим собой, имеется естественная структура ChartedSpace через идентичный атлас.

LaTeX

$$chartedSpaceSelf (H) (M) ...$$

Lean4

/-- In the trivial `ChartedSpace` structure of a space modelled over itself through the identity,
the atlas members are just the identity. -/
@[simp, mfld_simps]
theorem chartedSpaceSelf_atlas {H : Type*} [TopologicalSpace H] {e : OpenPartialHomeomorph H H} :
    e ∈ atlas H H ↔ e = OpenPartialHomeomorph.refl H :=
  Iff.rfl

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