Documentation

Mathlib.Topology.MetricSpace.ProperSpace

Proper spaces #

Main definitions and results #

class ProperSpace (α : Type u) [PseudoMetricSpace α] :

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

Instances
    theorem isCompact_sphere {α : Type u_3} [PseudoMetricSpace α] [ProperSpace α] (x : α) (r : ) :

    In a proper pseudometric space, all spheres are compact.

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

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

    Equations
    • =
    @[instance 100]

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

    Equations
    • =
    theorem ProperSpace.of_isCompact_closedBall_of_le {α : Type u} [PseudoMetricSpace α] (R : ) (h : ∀ (x : α) (r : ), R rIsCompact (Metric.closedBall x 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} [PseudoMetricSpace α] (R : ) (h : ∀ (x : α) (r : ), R rIsCompact (Metric.closedBall x 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} [PseudoMetricSpace α] {β : Type u_3} {l : Filter β} [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]
    Equations
    • =
    @[instance 100]

    A proper space is locally compact

    Equations
    • =
    @[instance 100]

    A proper space is complete

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

    A binary product of proper spaces is proper.

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

    A finite product of proper spaces is proper.

    Equations
    • =
    Equations
    • = inst