The set of points where a map is C^n #
For n ≠ ∞, a map between manifolds is C^n at a point if and only if it is C^n on a
neighbourhood of that point (contMDiffAt_iff_contMDiffAt_nhds), so the set of points where it
is C^n is open. This file records that openness.
It also records that the regularity indices ∞ and ω are nonzero, as NeZero instances, so
that statements about C^n manifolds assuming [NeZero n] (that is, 1 ≤ n) apply to smooth
and analytic manifolds.
Main results #
TauCeti.isOpen_setOfPred_contMDiffAt: forn ≠ ∞, the set of points where a map isC^nis open.- The instances
NeZero (∞ : ℕ∞ω)andNeZero (ω : ℕ∞ω).
The smoothness index ∞ is nonzero, so smooth manifolds are differentiable.
The analyticity index ω is nonzero, so analytic manifolds are differentiable.
theorem
TauCeti.isOpen_setOfPred_contMDiffAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{n : WithTop ℕ∞}
{f : M → M'}
[IsManifold I n M]
[IsManifold I' n M']
(hn : n ≠ ↑⊤)
:
For n ≠ ∞, the set of points where a map is C^n is open. This fails for n = ∞, where
the neighbourhood on which f is C^k may shrink with k.