singletonChartedSpace — Mathlib

English

If e is a chart on M with source all of α, then the chart at x for the singleton charted space equals e.

Русский

Если e — чарт на M с источником всего α, то chartAt для единичного пространства равен e.

LaTeX

$$@chartAt H x = e, where e = (e.singletonChartedSpace h)$$

Lean4

/-- If a single open partial homeomorphism `e` from a space `α` into `H` has source covering the
whole space `α`, then that open partial homeomorphism induces an `H`-charted space structure on `α`.
(This condition is equivalent to `e` being an open embedding of `α` into `H`; see
`IsOpenEmbedding.singletonChartedSpace`.) -/
def singletonChartedSpace (h : e.source = Set.univ) : ChartedSpace H α
    where
  atlas := { e }
  chartAt _ := e
  mem_chart_source _ := by rw [h]; apply mem_univ
  chart_mem_atlas _ := by tauto

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