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
    • =
    theorem exists_pos_lt_subset_ball {α : Type u} [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} [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} {β : Type v} [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') :
    zMetric.ball a r, IsLocalMin f z
    Equations
    • = inst