# 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 ProperSpace.isCompact_closedBall {α : Type u} [self : ] (x : α) (r : ) :
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 100]
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 : } [l.NeBot] {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 100]
instance proper_of_compact {α : Type u} [] :
Equations
• =
@[instance 100]
instance locally_compact_of_proper {α : Type u} [] :

A proper space is locally compact

Equations
• =
@[instance 100]
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
• =
instance instProperSpaceAdditive {X : Type u_1} [] :
Equations
• = inst
instance instProperSpaceMultiplicative {X : Type u_1} [] :
Equations
• = inst
instance instProperSpaceOrderDual {X : Type u_1} [] :
Equations
• = inst