singletonChartedSpace_chartAt_eq — Mathlib

English

The source of the singleton-charted-space chart is the whole space, i.e., its source is Set.univ.

Русский

Источник чарта единичного пространства равен всему пространству: Set.univ.

LaTeX

$$(@chartAt H _ α _ (e.singletonChartedSpace h) x).source = Set.univ$$

Lean4

@[simp, mfld_simps]
theorem singletonChartedSpace_chartAt_eq (h : e.source = Set.univ) {x : α} :
    @chartAt H _ α _ (e.singletonChartedSpace h) x = e :=
  rfl

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