chartedSpaceSelf — Mathlib

English

In the identity-charted space, atlas elements are exactly identities.

Русский

В пространстве с идентичной картой атлас равен тождественному отображению.

LaTeX

$$@[simp] chartedSpaceSelf_atlas$$

Lean4

/-- Any space is a `ChartedSpace` modelled over itself, by just using the identity chart. -/
instance chartedSpaceSelf (H : Type*) [TopologicalSpace H] : ChartedSpace H H
    where
  atlas := {OpenPartialHomeomorph.refl H}
  chartAt _ := OpenPartialHomeomorph.refl H
  mem_chart_source x := mem_univ x
  chart_mem_atlas _ := mem_singleton _

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