Proper spaces #
This file contains some more involved results about ProperSpaces.
Main definitions and results #
theorem
exists_pos_lt_subset_ball
{α : Type u_1}
[PseudoMetricSpace α]
[ProperSpace α]
{x : α}
{r : ℝ}
{s : Set α}
(hr : 0 < r)
(hs : IsClosed s)
(h : s ⊆ Metric.ball x r)
:
∃ r' ∈ Set.Ioo 0 r, s ⊆ Metric.ball x r'
If a nonempty ball in a proper space includes a closed set s, then there exists a nonempty
ball with the same center and a strictly smaller radius that includes s.
theorem
exists_lt_subset_ball
{α : Type u_1}
[PseudoMetricSpace α]
[ProperSpace α]
{x : α}
{r : ℝ}
{s : Set α}
(hs : IsClosed s)
(h : s ⊆ Metric.ball x r)
:
∃ r' < r, s ⊆ Metric.ball x r'
If a ball in a proper space includes a closed set s, then there exists a ball with the same
center and a strictly smaller radius that includes s.
theorem
Metric.exists_isLocalMin_mem_ball
{α : Type u_1}
{β : Type u_2}
[PseudoMetricSpace α]
[ProperSpace α]
[TopologicalSpace β]
[ConditionallyCompleteLinearOrder β]
[OrderTopology β]
{f : α → β}
{a : α}
{z : α}
{r : ℝ}
(hf : ContinuousOn f (Metric.closedBall a r))
(hz : z ∈ Metric.closedBall a r)
(hf1 : ∀ z' ∈ Metric.sphere a r, f z < f z')
:
∃ z ∈ Metric.ball a r, IsLocalMin f z