# Documentation

## Main definitions and results #

• ProperSpace α: a PseudoMetricSpace where all closed balls are compact

• isCompact_sphere: any sphere in a proper space is compact.

• proper_of_compact: compact spaces are proper.

• secondCountable_of_proper: proper spaces are sigma-compact, hence second countable.

• locally_compact_of_proper: proper spaces are locally compact.

• pi_properSpace: finite products of proper spaces are proper.

class ProperSpace (α : Type u) :

A pseudometric space is proper if all closed balls are compact.

• isCompact_closedBall : ∀ (x : α) (r : ),
Instances
theorem isCompact_sphere {α : Type u_3} [] (x : α) (r : ) :

In a proper pseudometric space, all spheres are compact.

instance Metric.sphere.compactSpace {α : Type u_3} [] (x : α) (r : ) :

In a proper pseudometric space, any sphere is a CompactSpace when considered as a subtype.

Equations
• =
instance secondCountable_of_proper {α : Type u} [] :

A proper pseudo metric space is sigma compact, and therefore second countable.

Equations
• =
theorem ProperSpace.of_isCompact_closedBall_of_le {α : Type u} (R : ) (h : ∀ (x : α) (r : ), R r) :

If all closed balls of large enough radius are compact, then the space is proper. Especially useful when the lower bound for the radius is 0.

@[deprecated ProperSpace.of_isCompact_closedBall_of_le]
theorem properSpace_of_compact_closedBall_of_le {α : Type u} (R : ) (h : ∀ (x : α) (r : ), R r) :

Alias of ProperSpace.of_isCompact_closedBall_of_le.

If all closed balls of large enough radius are compact, then the space is proper. Especially useful when the lower bound for the radius is 0.

theorem ProperSpace.of_seq_closedBall {α : Type u} {β : Type u_3} {l : } [] {x : α} {r : β} (hr : Filter.Tendsto r l Filter.atTop) (hc : ∀ᶠ (i : β) in l, IsCompact (Metric.closedBall x (r i))) :

If there exists a sequence of compact closed balls with the same center such that the radii tend to infinity, then the space is proper.

instance proper_of_compact {α : Type u} [] :
Equations
• =
instance locally_compact_of_proper {α : Type u} [] :

A proper space is locally compact

Equations
• =
instance complete_of_proper {α : Type u} [] :

A proper space is complete

Equations
• =
instance prod_properSpace {α : Type u_3} {β : Type u_4} [] [] :
ProperSpace (α × β)

A binary product of proper spaces is proper.

Equations
• =
instance pi_properSpace {β : Type v} {π : βType u_3} [] [(b : β) → PseudoMetricSpace (π b)] [h : ∀ (b : β), ProperSpace (π b)] :
ProperSpace ((b : β) → π b)

A finite product of proper spaces is proper.

Equations
• =
theorem exists_pos_lt_subset_ball {α : Type u} [] {x : α} {r : } {s : Set α} (hr : 0 < r) (hs : ) (h : s ) :
∃ 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} [] {x : α} {r : } {s : Set α} (hs : ) (h : s ) :
∃ 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} {β : Type v} [] [] [] {f : αβ} {a : α} {z : α} {r : } (hf : ) (hz : z ) (hf1 : z', f z < f z') :
∃ z ∈ ,