English
The disjoint union of two C^n manifolds, modeled on the same space (E,H), is itself a C^n manifold under the same model I.
Русский
Непересекающееся объединение двух C^n-многообразий, моделируемых на той же модели (E,H), тоже является C^n-многообразием по той же модели I.
LaTeX
$$IsManifold I n M ∧ IsManifold I n M' ⇒ IsManifold I n (Sum M M')$$
Lean4
/-- The disjoint union of two `C^n` manifolds modelled on `(E, H)`
is a `C^n` manifold modeled on `(E, H)`. -/
instance disjointUnion : IsManifold I n (M ⊕ M') where
compatible {e} e' he
he' := by
obtain (h | h) := isEmpty_or_nonempty H
· exact ContDiffGroupoid.mem_of_source_eq_empty _ (eq_empty_of_isEmpty _)
obtain (⟨f, hf, hef⟩ | ⟨f, hf, hef⟩) := ChartedSpace.mem_atlas_sum he
· obtain (⟨f', hf', he'f'⟩ | ⟨f', hf', he'f'⟩) := ChartedSpace.mem_atlas_sum he'
· rw [hef, he'f', f.lift_openEmbedding_trans f' IsOpenEmbedding.inl]
exact hM.compatible hf hf'
· rw [hef, he'f']
apply ContDiffGroupoid.mem_of_source_eq_empty
ext x
exact ⟨fun ⟨hx₁, hx₂⟩ ↦ by simp_all, fun hx ↦ hx.elim⟩
· -- Analogous argument to the first case: is there a way to deduplicate?
obtain (⟨f', hf', he'f'⟩ | ⟨f', hf', he'f'⟩) := ChartedSpace.mem_atlas_sum he'
· rw [hef, he'f']
apply ContDiffGroupoid.mem_of_source_eq_empty
ext x
exact ⟨fun ⟨hx₁, hx₂⟩ ↦ by simp_all, fun hx ↦ hx.elim⟩
· rw [hef, he'f', f.lift_openEmbedding_trans f' IsOpenEmbedding.inr]
exact hM'.compatible hf hf'
