instChartedSpace — Mathlib

English

An open subset s of a charted space naturally inherits a charted space structure.

Русский

Открытое подмножество s чартизированного пространства естественно наследует структуру чартизированного пространства.

LaTeX

$$TopologicalSpace.Opens.instChartedSpace$$

Lean4

/-- An open subset of a charted space is naturally a charted space. -/
protected instance instChartedSpace : ChartedSpace H s
    where
  atlas := ⋃ x : s, {(chartAt H x.1).subtypeRestr ⟨x⟩}
  chartAt x := (chartAt H x.1).subtypeRestr ⟨x⟩
  mem_chart_source x := ⟨trivial, mem_chart_source H x.1⟩
  chart_mem_atlas
    x := by
    simp only [mem_iUnion, mem_singleton_iff]
    use x

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