Zero-dimensional analytic submanifolds

A zero-dimensional analytic submanifold is discrete, and every nonempty discrete subset of a finite-dimensional scalar space is a zero-dimensional analytic submanifold. In particular, a preconnected zero-dimensional analytic submanifold consists of one point. This identifies the bases on which polynomial lifting can use a refinement over a single point.

The chart condition is essential: a totally disconnected set need not be discrete. Neither finiteness nor closedness of the submanifold is required.

References

S. G. Krantz and H. R. Parks, A Primer of Real Analytic Functions, second edition, Birkhäuser, 2002, Chapter 2 (analytic submanifolds).

theorem TauCeti.IsAnalyticSubmanifold.isDiscrete {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : ℕ} {S : Set (Fin n → 𝕜)} (hS : IsAnalyticSubmanifold 0 S) : IsDiscrete S

A zero-dimensional analytic submanifold is discrete in its subspace topology.

theorem IsDiscrete.isAnalyticSubmanifold_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : ℕ} {S : Set (Fin n → 𝕜)} (hS : IsDiscrete S) (hne : S.Nonempty) : TauCeti.IsAnalyticSubmanifold 0 S

Every nonempty discrete subset is a zero-dimensional analytic submanifold. The ambient charts are translations restricted to isolating neighborhoods.

@[simp]

theorem TauCeti.isAnalyticSubmanifold_zero_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : ℕ} {S : Set (Fin n → 𝕜)} : IsAnalyticSubmanifold 0 S ↔ S.Nonempty ∧ IsDiscrete S

Zero-dimensional analytic submanifolds are precisely the nonempty discrete subsets.