English
Given a charted-space core without topology, one obtains a genuine charted-space structure on M by generating a topology from its atlas and by defining charts via the openPartialHomeomorph objects attached to atlas members.
Русский
Дано ядро чартизованного пространства без топологии; получаем подлинную структуру чартизованного пространства на M, генерируя топологию из атласа и задавая карты через открытые частичные гомоморфизмы, связанные с членами атласа.
LaTeX
$$$\text{toChartedSpace}(c) = \big( M, \text{atlas} = \bigcup_{e\in c.atlas} \{ c.openPartialHomeomorph\ e\;\}, \text{chartAt}(x) = c.openPartialHomeomorph\ (c.chartAt\ x)\ (c.chart\_mem\_atlas\ x), \text{mem\_chart\_source} = c.mem\_chart\_source, \text{chart\_mem\_atlas} = c.chart\_mem\_atlas \big).$$$
Lean4
/-- Topology generated by a set of charts on a Type. -/
protected def toTopologicalSpace : TopologicalSpace M :=
TopologicalSpace.generateFrom <|
⋃ (e : PartialEquiv M H) (_ : e ∈ c.atlas) (s : Set H) (_ : IsOpen s), {e ⁻¹' s ∩ e.source}
