Regular points form an open set #
A point is a regular point of a map when its manifold derivative there is surjective
(TauCeti.IsRegularPoint). For a C¹ map into a manifold modelled on a finite-dimensional space,
regularity is an open condition: the regular points are the points of maximal rank
(TauCeti.isRegularPoint_iff_mfderivRank_eq), and the rank of a C¹ map can only go up near a
point (TauCeti.eventually_mfderivRank_le_mfderivRank). So the set of regular points of a C¹ map
is open, and a dense set of regular points is a dense open set.
Main results #
TauCeti.IsRegularPoint.eventually_isRegularPoint: the points near a regular point of aC¹map are regular.TauCeti.isOpen_setOf_isRegularPoint: the regular points of aC¹map form an open set.
References #
- J. M. Lee, Introduction to Smooth Manifolds, 2nd ed., Graduate Texts in Mathematics 218, Springer, 2013, Proposition 4.1 (submersion points form an open set).
theorem
TauCeti.IsRegularPoint.eventually_isRegularPoint
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
[CompleteSpace 𝕜]
{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]
[IsManifold I 1 M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
[FiniteDimensional 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{J : ModelWithCorners 𝕜 E' H'}
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace H' N]
[IsManifold J 1 N]
{f : M → N}
{x : M}
{n : WithTop ℕ∞}
(h : IsRegularPoint I J f x)
(hf : ContMDiffAt I J n f x)
(hn : 1 ≤ n)
:
∀ᶠ (y : M) in nhds x, IsRegularPoint I J f y
Regularity is an open condition. Every point near a regular point of a map which is C¹
there is a regular point.
theorem
TauCeti.isOpen_setOf_isRegularPoint
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
[CompleteSpace 𝕜]
{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]
[IsManifold I 1 M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
[FiniteDimensional 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{J : ModelWithCorners 𝕜 E' H'}
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace H' N]
[IsManifold J 1 N]
{f : M → N}
{n : WithTop ℕ∞}
(hf : ContMDiff I J n f)
(hn : 1 ≤ n)
:
The regular points of a C¹ map form an open set.