English
If H is nonempty and e ∈ atlas H (M ⊕ M'), then e is either obtained by lifting a chart from M or from M' via the left or right embedding.
Русский
Если H непусто и e принадлежит atlas H (M ⊕ M'), то e получается либо за счёт левой, либо правой инъекции.
LaTeX
$$$\text{If } h:\,\text{Nonempty}(H)\text{ and } e\in atlas(H,(M\oplus M')) ,\;\text{then }\; e = (f.lift\_openEmbedding\ IsOpenEmbedding.inl)\text{ for some } f\in atlas(H,M)\text{ or } e = (f'.lift\_openEmbedding\ IsOpenEmbedding.inr)\text{ for some } f'\in atlas(H,M').$$$
Lean4
theorem mem_atlas_sum [h : Nonempty H] {e : OpenPartialHomeomorph (M ⊕ M') H} (he : e ∈ atlas H (M ⊕ M')) :
(∃ f : OpenPartialHomeomorph M H, f ∈ (atlas H M) ∧ e = (f.lift_openEmbedding IsOpenEmbedding.inl)) ∨
(∃ f' : OpenPartialHomeomorph M' H, f' ∈ (atlas H M') ∧ e = (f'.lift_openEmbedding IsOpenEmbedding.inr)) :=
by
simp only [atlas, sum, h, ↓reduceDIte] at he
obtain (⟨x, hx, hxe⟩ | ⟨x, hx, hxe⟩) := he
· rw [← hxe]; left; use x
· rw [← hxe]; right; use x
