singletonChartedSpace_chartAt_source

English

If e' is in the atlas of the singleton-charted-space of e with source all of α, then e' = e.

Русский

Если e' принадлежит атласу единичного чарта e, где источник — вся α, то e' = e.

LaTeX

$$e' \in (e.singletonChartedSpace h).atlas \Rightarrow e' = e$$

Lean4

theorem singletonChartedSpace_chartAt_source (h : e.source = Set.univ) {x : α} :
    (@chartAt H _ α _ (e.singletonChartedSpace h) x).source = Set.univ :=
  h

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