English
For every x ∈ M, the chartAt H x belongs to the maximal atlas for I, n, M.
Русский
Для каждого x ∈ M диаграмма chartAt H x принадлежит максимальному атласу для I, n, M.
LaTeX
$$chartAt(H,x) ∈ maximalAtlas(I,n,M)$$
Lean4
/-- The empty set is a `C^n` manifold w.r.t. any charted space and model. -/
instance empty [IsEmpty M] : IsManifold I n M :=
by
apply isManifold_of_contDiffOn
intro e e' _ _ x hx
set t := I.symm ⁻¹' (e.symm ≫ₕ e').source ∩ range I
have : (e.symm ≫ₕ e').source = ∅ :=
calc
(e.symm ≫ₕ e').source
_ = (e.symm.source) ∩ e.symm ⁻¹' e'.source := by rw [← OpenPartialHomeomorph.trans_source]
_ = (e.symm.source) ∩ e.symm ⁻¹' ∅ := by rw [eq_empty_of_isEmpty (e'.source)]
_ = (e.symm.source) ∩ ∅ := by rw [preimage_empty]
_ = ∅ := inter_empty e.symm.source
have : t = ∅ :=
calc
t
_ = I.symm ⁻¹' (e.symm ≫ₕ e').source ∩ range I := by rw [← Subtype.preimage_val_eq_preimage_val_iff]
_ = ∅ ∩ range I := by rw [this, preimage_empty]
_ = ∅ := empty_inter (range I)
apply (this ▸ hx).elim
