def
ChartedSpace.ball
{𝕜 : Type u_1}
{E : Type u_2}
{M : Type u_3}
{H : Type u_4}
[NontriviallyNormedField 𝕜]
[TopologicalSpace H]
[TopologicalSpace M]
[ChartedSpace H M]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
(I : ModelWithCorners 𝕜 E H)
(x : M)
(r : ℝ)
:
Set M
If M is a ChartedSpace we can use the preferred chart at any point to transfer a
ball in coordinate space into a set in M. These can be a useful neighbourhood basis.
Equations
- ChartedSpace.ball I x r = ↑(extChartAt I x).symm '' Metric.ball (↑(extChartAt I x) x) r
Instances For
theorem
ChartedSpace.nhds_hasBasis_balls_of_open_cov
{𝕜 : Type u_1}
{E : Type u_2}
{M : Type u_3}
{H : Type u_4}
[NontriviallyNormedField 𝕜]
[TopologicalSpace H]
[TopologicalSpace M]
[ChartedSpace H M]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
(I : ModelWithCorners 𝕜 E H)
[I.Boundaryless]
(x : M)
{ι : Type u_5}
{s : ι → Set M}
(s_op : ∀ (j : ι), IsOpen (s j))
(cov : ⋃ (j : ι), s j = Set.univ)
:
(nhds x).HasBasis
(fun (r : ℝ) => 0 < r ∧ Metric.ball (↑(extChartAt I x) x) r ⊆ (extChartAt I x).target ∧ ∃ (j : ι), ball I x r ⊆ s j)
(ball I x)