Lean4
/-- The disjoint union of two charted spaces modelled on a non-empty space `H`
is a charted space over `H`. -/
def sum_of_nonempty [Nonempty H] : ChartedSpace H (M ⊕ M')
where
atlas :=
((fun e ↦ e.lift_openEmbedding IsOpenEmbedding.inl) '' cm.atlas) ∪
((fun e ↦ e.lift_openEmbedding IsOpenEmbedding.inr) '' cm'.atlas)
-- At `x : M`, the chart is the chart in `M`; at `x' ∈ M'`, it is the chart in `M'`.
chartAt :=
Sum.elim (fun x ↦ (cm.chartAt x).lift_openEmbedding IsOpenEmbedding.inl)
(fun x ↦ (cm'.chartAt x).lift_openEmbedding IsOpenEmbedding.inr)
mem_chart_source
p := by
cases p with
| inl
x =>
rw [Sum.elim_inl, lift_openEmbedding_source, ←
OpenPartialHomeomorph.lift_openEmbedding_source _ IsOpenEmbedding.inl]
use x, cm.mem_chart_source x
| inr
x =>
rw [Sum.elim_inr, lift_openEmbedding_source, ←
OpenPartialHomeomorph.lift_openEmbedding_source _ IsOpenEmbedding.inr]
use x, cm'.mem_chart_source x
chart_mem_atlas
p := by
cases p with
| inl x =>
rw [Sum.elim_inl]
left
use ChartedSpace.chartAt x, cm.chart_mem_atlas x
| inr x =>
rw [Sum.elim_inr]
right
use ChartedSpace.chartAt x, cm'.chart_mem_atlas x
