isCompact_sphere
theorem isCompact_sphere :
∀ {α : Type u_3} [inst : PseudoMetricSpace α] [inst_1 : ProperSpace α] (x : α) (r : ℝ),
IsCompact (Metric.sphere x r)
The theorem `isCompact_sphere` states that in a proper pseudometric space, all spheres are compact. In other words, for any point `x` and any real number `r`, the set of all points at a distance `r` from `x` (defined as `Metric.sphere x r`) is compact. Here, a set is considered compact if, for every nontrivial filter that contains the set, there exists a point in the set such that every set of the filter intersects with every neighborhood of that point. A proper pseudometric space is a topological space that satisfies certain mathematical properties related to distance.
More concisely: In a proper pseudometric space, every metric ball is compact.
|
properSpace_of_compact_closedBall_of_le
theorem properSpace_of_compact_closedBall_of_le :
∀ {α : Type u} [inst : PseudoMetricSpace α] (R : ℝ),
(∀ (x : α) (r : ℝ), R ≤ r → IsCompact (Metric.closedBall x r)) → ProperSpace α
This theorem, referenced as `properSpace_of_compact_closedBall_of_le`, states that a space is proper if all closed balls with a radius greater than or equal to a certain real number `R` are compact. This is particularly useful when the lower bound for the radius is 0. In this context, a closed ball in a pseudometric space is the set of all points `y` such that the distance between `y` and the center of the ball `x` is less than or equal to the radius. A set is considered to be compact if for every nontrivial filter that contains the set, there exists a point in the set such that every set of the filter meets every neighborhood of the point.
More concisely: A pseudometric space is proper if all closed balls with radius greater than or equal to a certain real number have compact closure.
|
exists_pos_lt_subset_ball
theorem exists_pos_lt_subset_ball :
∀ {α : Type u} [inst : PseudoMetricSpace α] [inst_1 : ProperSpace α] {x : α} {r : ℝ} {s : Set α},
0 < r → IsClosed s → s ⊆ Metric.ball x r → ∃ r' ∈ Set.Ioo 0 r, s ⊆ Metric.ball x r'
This theorem states that for any nonempty ball in a proper metric space, if this ball encompasses a closed set, then there exists another nonempty ball with the same center but with a strictly smaller radius that also encompasses this closed set. In more formal terms, given a proper metric space `α`, a point `x` in `α`, a positive real number `r`, and a closed set `s` of `α` such that `s` is completely contained in the open ball of radius `r` centered at `x`, there exists a positive real number `r'` in the open interval `(0, r)`, such that `s` is also completely contained in the open ball of radius `r'` centered at `x`.
More concisely: Given a proper metric space, a point, a closed set completely contained in the open ball around that point, there exists a smaller open ball with the same center that also encompasses the closed set.
|
ProperSpace.of_seq_closedBall
theorem ProperSpace.of_seq_closedBall :
∀ {α : Type u} [inst : PseudoMetricSpace α] {β : Type u_3} {l : Filter β} [inst_1 : l.NeBot] {x : α} {r : β → ℝ},
Filter.Tendsto r l Filter.atTop → (∀ᶠ (i : β) in l, IsCompact (Metric.closedBall x (r i))) → ProperSpace α
This theorem states that in a pseudometric space, if there exists a sequence of compact closed balls with a common center, and the radii of these balls tend to infinity, then the space is proper. A proper space is one in which every closed ball is compact. In other words, if you can find a sequence of balls centered at a particular point, such that these balls get arbitrarily large and each one is compact, then the entire space is proper.
More concisely: In a pseudometric space, if there exists a sequence of compact closed balls with a common center and radii tending to infinity, then the space is proper (every closed ball is compact).
|
ProperSpace.of_isCompact_closedBall_of_le
theorem ProperSpace.of_isCompact_closedBall_of_le :
∀ {α : Type u} [inst : PseudoMetricSpace α] (R : ℝ),
(∀ (x : α) (r : ℝ), R ≤ r → IsCompact (Metric.closedBall x r)) → ProperSpace α
The theorem `ProperSpace.of_isCompact_closedBall_of_le` states that for a given type `α` that has a pseudo metric space structure, if for all points `x` in `α` and for all radii `r` greater than or equal to a radius `R`, the closed ball centered at `x` with radius `r` is compact, then `α` is a proper space. This theorem is particularly useful when the lower bound for the radius is zero. In other words, if every closed ball of sufficiently large radius in a given space is a compact set, then the space is a proper metric space.
More concisely: If every closed ball in a metric space with radius greater than or equal to a certain limit is compact, then the space is proper.
|
exists_lt_subset_ball
theorem exists_lt_subset_ball :
∀ {α : Type u} [inst : PseudoMetricSpace α] [inst_1 : ProperSpace α] {x : α} {r : ℝ} {s : Set α},
IsClosed s → s ⊆ Metric.ball x r → ∃ r' < r, s ⊆ Metric.ball x r'
This theorem, `exists_lt_subset_ball`, states that for any type `α` that is a `PseudoMetricSpace` and a `ProperSpace`, given a point `x` of type `α`, a real number `r`, and a closed set `s` of type `α`, if `s` is a subset of the ball with center `x` and radius `r`, then there exists a real number `r'` that is strictly less than `r`, such that `s` is also a subset of the ball with center `x` and radius `r'`.
In other words, if a closed set is contained within a certain ball in a proper space, there is another ball with the same center and a smaller radius that also contains this closed set.
More concisely: Given a `PseudoMetricSpace` and `ProperSpace` TYPE `α` with point `x`, real number `r`, and closed set `s`, if `s ⊆ ball x r`, then there exists `r' < r` such that `s ⊆ ball x r'`.
|