Proper spaces

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.

• locallyCompact_of_proper: proper spaces are locally compact.

• pi_properSpace: finite products of proper spaces are proper.

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

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

• isCompact_closedBall (x : α) (r : ℝ) : IsCompact (Metric.closedBall x r)

Instances

• Complex.instProperSpace
• FiniteDimensional.RCLike.properSpace_submodule
• FiniteDimensional.proper_real
• Int.instProperSpace
• NNReal.instProperSpace
• Nat.instProperSpace
• instProperSpaceAdditive
• instProperSpaceMultiplicative
• instProperSpaceOrderDual
• instProperSpaceReal
• instProperSpaceSubtypeMemSubmoduleOfCompleteSpaceOfLocallyCompactSpace
• pi_properSpace
• prod_properSpace
• proper_of_compact

theorem isCompact_sphere {α : Type u_3} [PseudoMetricSpace α] [ProperSpace α] (x : α) (r : ℝ) : IsCompact (Metric.sphere x r)

In a proper pseudometric space, all spheres are compact.

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

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

@[instance 100]

instance secondCountable_of_proper {α : Type u} [PseudoMetricSpace α] [ProperSpace α] : SecondCountableTopology α

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

theorem ProperSpace.of_isCompact_closedBall_of_le {α : Type u} [PseudoMetricSpace α] (R : ℝ) (h : ∀ (x : α) (r : ℝ), R ≤ r → IsCompact (Metric.closedBall x r)) : ProperSpace α

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))) : ProperSpace α

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} [PseudoMetricSpace α] [CompactSpace α] : ProperSpace α

@[instance 100]

instance locallyCompact_of_proper {α : Type u} [PseudoMetricSpace α] [ProperSpace α] : LocallyCompactSpace α

A proper space is locally compact

@[deprecated locallyCompact_of_proper (since := "2024-11-13")]

theorem locally_compact_of_proper {α : Type u} [PseudoMetricSpace α] [ProperSpace α] : LocallyCompactSpace α

Alias of locallyCompact_of_proper.

---

A proper space is locally compact

@[instance 100]

instance complete_of_proper {α : Type u} [PseudoMetricSpace α] [ProperSpace α] : CompleteSpace α

A proper space is complete

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

A binary product of proper spaces is proper.

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.

theorem ProperSpace.of_isClosed {X : Type u_3} [PseudoMetricSpace X] [ProperSpace X] {s : Set X} (hs : IsClosed s) : ProperSpace ↑s

A closed subspace of a proper space is proper. This is true for any proper lipschitz map. See LipschitzWith.properSpace.

instance instProperSpaceAdditive {X : Type u_1} [PseudoMetricSpace X] [ProperSpace X] : ProperSpace (Additive X)

instance instProperSpaceMultiplicative {X : Type u_1} [PseudoMetricSpace X] [ProperSpace X] : ProperSpace (Multiplicative X)

instance instProperSpaceOrderDual {X : Type u_1} [PseudoMetricSpace X] [ProperSpace X] : ProperSpace Xᵒᵈ