English
The sum (coproduct) of two charted spaces over a fixed model space H is again a charted space over H. If H is nonempty, use the standard sum; if H is empty, then both M and M' are empty and the sum is empty.
Русский
Сумма (копродукт) двух чартизированных пространств над фиксированым моделирующим пространством H снова образует чартизованное пространство над H. При непустом H применяется обычная сумма; если H пусто, то M и M' пусты и сумма пустая.
LaTeX
$$$\text{ChartedSpace } H (M \oplus M') = \begin{cases} \text{ChartedSpace.sum_of_nonempty } H (M) (M'), & \text{если } \text{Nonempty}(H) \\ \text{ChartedSpace.empty } H (M \oplus M'), & \text{иначе} \end{cases}.$$$
Lean4
instance sum : ChartedSpace H (M ⊕ M') :=
if h : Nonempty H then ChartedSpace.sum_of_nonempty
else by
push_neg at h
have : IsEmpty M := isEmpty_of_chartedSpace H
have : IsEmpty M' := isEmpty_of_chartedSpace H
exact empty H (M ⊕ M')
