English
The construction toChartedSpace(c) satisfies the defining properties of a charted-space structure on M with atlas built from the openPartialHomeomorphs attached to the atlas of c.
Русский
Построение toChartedSpace(c) удовлетворяет определяющим свойствам чартизованного пространства на M с атласом, составленным из соответствующих открытых частичных гомоморфизмов.
LaTeX
$$$\text{toChartedSpace}(c)\ ext{defines a charted-space structure on } M$ with atlas $\bigcup_{e\in c.atlas} \{c.openPartialHomeomorph e\}$ and chartAt as given.$$
Lean4
/-- Given a charted space without topology, endow it with a genuine charted space structure with
respect to the topology constructed from the atlas. -/
def toChartedSpace : @ChartedSpace H _ M c.toTopologicalSpace :=
{ __ := c.toTopologicalSpace
atlas := ⋃ (e : PartialEquiv M H) (he : e ∈ c.atlas), {c.openPartialHomeomorph e he}
chartAt := fun x ↦ c.openPartialHomeomorph (c.chartAt x) (c.chart_mem_atlas x)
mem_chart_source := fun x ↦ c.mem_chart_source x
chart_mem_atlas := fun x ↦ by
simp only [mem_iUnion, mem_singleton_iff]
exact ⟨c.chartAt x, c.chart_mem_atlas x, rfl⟩ }
