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.

• locally_compact_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)

theorem ProperSpace.isCompact_closedBall {α : Type u} [PseudoMetricSpace α] [self : ProperSpace α] (x : α) (r : ℝ) : IsCompact (Metric.closedBall x r)

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 ↑(Metric.sphere 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} [PseudoMetricSpace α] [ProperSpace α] : SecondCountableTopology α

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 ≤ 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.

@[deprecated ProperSpace.of_isCompact_closedBall_of_le]

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

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

Equations

• ⋯ = ⋯

@[instance 100]

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

A proper space is locally compact

Equations

• ⋯ = ⋯

@[instance 100]

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

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') : ∃ z ∈ Metric.ball a r, IsLocalMin f z

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

Equations

• ⋯ = inst

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

Equations

• ⋯ = inst

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

Equations

• ⋯ = inst