Metric.isBounded_iff_ediam_ne_top
theorem Metric.isBounded_iff_ediam_ne_top :
∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α}, Bornology.IsBounded s ↔ EMetric.diam s ≠ ⊤
The theorem `Metric.isBounded_iff_ediam_ne_top` establishes a characterization of the boundedness of a set within a pseudometric space. Specifically, it states that for any set `s` in a type `α` under a pseudometric space structure, the set `s` is bounded relative to the ambient bornology on `α` if and only if the emetric (pseudoemetric) diameter of the set `s` is not infinity. In other words, a set is considered bounded in this context if and only if it doesn't have an infinite diameter in the pseudoemetric sense.
More concisely: A set in a pseudometric space is bounded if and only if its pseudometric diameter is finite.
|
Bornology.IsBounded.closure
theorem Bornology.IsBounded.closure :
∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α}, Bornology.IsBounded s → Bornology.IsBounded (closure s)
The theorem `Bornology.IsBounded.closure` states that for any type `α` that forms a pseudometric space and for any set `s` of type `α`, if `s` is bounded relative to the ambient bornology on `α`, then the closure of `s` (i.e., the smallest closed set containing `s`) is also bounded relative to the bornology on `α`. In other words, the property of being bounded is preserved under taking closures.
More concisely: If a set `s` in a pseudometric space `α` is bounded, then its closure is also bounded.
|
Bornology.IsBounded.isCompact_closure
theorem Bornology.IsBounded.isCompact_closure :
∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} [inst_1 : ProperSpace α],
Bornology.IsBounded s → IsCompact (closure s)
The Heine-Borel theorem states that in a proper space (a space in which every bounded subset is totally bounded), the closure of a bounded set is compact. Here, a set is said to be bounded if it is bounded relative to the ambient bornology on the space, and a set is compact if for every nontrivial filter that contains the set, there exists an element in the set such that every set of the filter meets every neighborhood of this element. The closure of a set is defined as the smallest closed set containing the set. In other words, in a space where boundedness is equivalent to total boundedness, making a bounded set closed (by taking its closure) makes it compact.
More concisely: In a proper space, the closure of a bounded set is compact.
|
IsComplete.nonempty_iInter_of_nonempty_biInter
theorem IsComplete.nonempty_iInter_of_nonempty_biInter :
∀ {α : Type u} [inst : PseudoMetricSpace α] {s : ℕ → Set α},
IsComplete (s 0) →
(∀ (n : ℕ), IsClosed (s n)) →
(∀ (n : ℕ), Bornology.IsBounded (s n)) →
(∀ (N : ℕ), (⋂ n, ⋂ (_ : n ≤ N), s n).Nonempty) →
Filter.Tendsto (fun n => Metric.diam (s n)) Filter.atTop (nhds 0) → (⋂ n, s n).Nonempty
This theorem states that for a sequence of sets in a pseudo-metric space, if each set in the sequence is complete, closed, and bounded, and the intersection of any finite subsequence is non-empty, then the intersection of the entire sequence is non-empty if the diameter of the sets in the sequence tends to zero. This scenario can occur in the study of limits in metric spaces where you want to ensure that the intersection of certain sets is not empty.
More concisely: If $(S\_n)_{n \in \mathbb{N}}$ is a sequence of non-empty, complete, closed, and bounded sets in a pseudo-metric space, such that the diameter of $S\_n$ tends to 0 and the intersection of any finite subsequence is non-empty, then $\bigcap\_{n \in \mathbb{N}} S\_n$ is non-empty.
|
Metric.exists_isOpen_isBounded_image_inter_of_isCompact_of_forall_continuousWithinAt
theorem Metric.exists_isOpen_isBounded_image_inter_of_isCompact_of_forall_continuousWithinAt :
∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : TopologicalSpace β] {k s : Set β} {f : β → α},
IsCompact k → (∀ x ∈ k, ContinuousWithinAt f s x) → ∃ t, k ⊆ t ∧ IsOpen t ∧ Bornology.IsBounded (f '' (t ∩ s))
The theorem states that given a function `f` from a topological space `β` to a pseudometric space `α`, a set `s` in `β`, and a compact set `k` in `β`, if `f` is continuous at every point of `k` within `s`, then there exists an open set `t` in `β` such that `k` is a subset of `t` and the image of the intersection of `t` and `s` under `f` is a bounded set in `α`. In other words, if a function is continuously mapped from each point of a compact set within a larger set, we can always find an open neighborhood of the compact set such that the function's image of the intersection of this neighborhood and the larger set is bounded.
More concisely: Given a continuous function from a compact set in a topological space to a pseudometric space, there exists an open neighborhood of the compact set with bounded image under the function.
|
Metric.exists_isOpen_isBounded_image_inter_of_isCompact_of_continuousOn
theorem Metric.exists_isOpen_isBounded_image_inter_of_isCompact_of_continuousOn :
∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : TopologicalSpace β] {k s : Set β} {f : β → α},
IsCompact k → k ⊆ s → ContinuousOn f s → ∃ t, k ⊆ t ∧ IsOpen t ∧ Bornology.IsBounded (f '' (t ∩ s))
This theorem states that if a function is continuous on a set `s` that contains a compact set `k`, then there exists an open neighborhood `t` of `k` such that `k` is a subset of `t`, and `t` is an open set in the ambient topological space, and the image of the intersection of `t` and `s` under the function `f` is bounded relative to the ambient bornology on the codomain of `f`.
In simpler terms, if we have a function that behaves in a 'smooth' manner on a set containing a compact set (a set that is both closed and bounded), then we can find an open neighborhood around that compact set where the function remains bounded. This theorem, therefore, combines concepts from topology (compactness and open sets) and analysis (boundedness and continuity) to describe a particular property of continuous functions.
More concisely: A continuous function on a set containing a compact subset maps that subset's open neighborhood to a bounded subset of its codomain.
|
TotallyBounded.isBounded
theorem TotallyBounded.isBounded :
∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α}, TotallyBounded s → Bornology.IsBounded s
This theorem states that for any set 's' in a pseudo-metric space 'α', if the set 's' is totally bounded, then it is also bounded with respect to the ambient bornology on 'α'. Here, a set is considered totally bounded if for any given entourage (a certain kind of neighborhood or measure of nearness), there exists a finite set of points such that every point in the set 's' is near to some point in this finite set according to the given entourage. A set is considered bounded in the bornology if its complement is co-bounded.
More concisely: In a pseudo-metric space, a totally bounded set is bounded with respect to the ambient bornology.
|
Metric.mem_cocompact_of_closedBall_compl_subset
theorem Metric.mem_cocompact_of_closedBall_compl_subset :
∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} [inst_1 : ProperSpace α] (c : α),
(∃ r, (Metric.closedBall c r)ᶜ ⊆ s) → s ∈ Filter.cocompact α
This theorem states that for any type `α` which is a pseudometric space and a proper space, and for any set `s` of type `α`, if there exists some real number `r` such that the complement of the set of all points within a distance `r` from a point `c` (represented as `Metric.closedBall c r`) is a subset of `s`, then `s` belongs to the collection of filters generated by complements of compact sets (represented as `Filter.cocompact α`). In other words, if `s` contains the outside of some closed ball in the pseudometric space, then `s` is in the filter of complements of compact sets.
More concisely: If `α` is a pseudometric and proper space, and for some `c` in `α` and real `r`, the complement of the closed ball `Metric.closedBall c r` is a subset of a set `s` in `α`, then `s` belongs to the filter of complements of compact sets `Filter.cocompact α`.
|
Metric.isBounded_ball
theorem Metric.isBounded_ball :
∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {r : ℝ}, Bornology.IsBounded (Metric.ball x r)
This theorem states that in any pseudometric space, the open balls are always bounded. Here, an open ball is defined as the set of all points that are at a distance less than a chosen radius from a given point. Boundedness is defined relative to the ambient bornology on the underlying set of the pseudometric space. Specifically, a set is said to be bounded if its complement is cobounded. In the context of this theorem, it means that no matter what point and radius we choose, the open ball with that center and radius is always a bounded set.
More concisely: In every pseudometric space, open balls are bounded.
|
Bornology.IsBounded.ediam_ne_top
theorem Bornology.IsBounded.ediam_ne_top :
∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α}, Bornology.IsBounded s → EMetric.diam s ≠ ⊤
This theorem, `Bornology.IsBounded.ediam_ne_top`, characterizes the boundedness of a set in terms of the finiteness of its emetric diameter within a pseudometric space. Specifically, it states that for any set `s` of type `α` in a pseudometric space, if `s` is bounded relative to the ambient bornology on `α` (i.e., `Bornology.IsBounded s` is true), then the emetric diameter of `s` is not infinite (`EMetric.diam s ≠ ⊤`).
More concisely: In a pseudometric space, a bounded set has finite metric diameter.
|
Metric.exists_isOpen_isBounded_image_of_isCompact_of_continuousOn
theorem Metric.exists_isOpen_isBounded_image_of_isCompact_of_continuousOn :
∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : TopologicalSpace β] {k s : Set β} {f : β → α},
IsCompact k → IsOpen s → k ⊆ s → ContinuousOn f s → ∃ t, k ⊆ t ∧ IsOpen t ∧ Bornology.IsBounded (f '' t)
This theorem states that if a function is continuous on a neighborhood of a compact set `k`, then the function is bounded on some open neighborhood of `k`. More formally, given a pseudometric space `α`, a topological space `β`, two subsets `k` and `s` of `β`, and a function `f` from `β` to `α`, if `k` is compact, `s` is an open set, and `k` is a subset of `s`, and the function `f` is continuous on `s`, then there exists an open set `t` such that `k` is a subset of `t` and the image of `t` under `f` is a bounded set.
More concisely: If a continuous function on an open neighborhood of a compact set is defined, then the function is bounded on some smaller open set containing the compact set.
|
Metric.isBounded_sphere
theorem Metric.isBounded_sphere :
∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {r : ℝ}, Bornology.IsBounded (Metric.sphere x r)
This theorem, titled "Metric.isBounded_sphere", states that in any pseudometric space `α`, for any point `x` in `α` and for any real number `r`, the sphere centered at `x` with radius `r` (which is the set of all points at a distance `r` from `x`) is a bounded set. Here, a set is considered bounded in the context of the ambient bornology on `α`. This means that there is a cobounded set in the bornology that contains the complement of our set, in this case, the sphere.
More concisely: In any pseudometric space, the sphere centered at a point with a finite radius is a bounded set.
|
Metric.dist_le_diam_of_mem
theorem Metric.dist_le_diam_of_mem :
∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} {x y : α},
Bornology.IsBounded s → x ∈ s → y ∈ s → dist x y ≤ Metric.diam s
This theorem states that for any type `α` with a `PseudoMetricSpace` instance, and for any set `s` of type `α` that is bounded (`Bornology.IsBounded`), if `x` and `y` are any two members of this set, then the distance between `x` and `y` is less than or equal to the diameter of the set `s`. In mathematical terms, if `s` is a bounded set in a pseudometric space and `x, y` are elements of `s`, then the distance between `x` and `y` (denoted `dist x y`) does not exceed the diameter of `s` (denoted `Metric.diam s`).
More concisely: In any pseudometric space with a bounded set `s`, the distance between any two elements of `s` is less than or equal to the diameter of `s`.
|
Metric.diam_nonneg
theorem Metric.diam_nonneg : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α}, 0 ≤ Metric.diam s
This theorem states that the diameter of a set is always nonnegative. Specifically, it asserts that for any type `α` that is a PseudoMetricSpace (a generalized metric space), and for any set `s` of elements of type `α`, the diameter of `s` (as computed by the `Metric.diam` function) is greater than or equal to 0. This means that in any metric space, the diameter, which is the greatest distance between any two points in the set, can never be a negative number.
More concisely: For any PseudoMetricSpace `α` and set `s` of elements in `α`, the diameter of `s` (as computed by `Metric.diam`) is a non-negative real number.
|
Metric.diam_union'
theorem Metric.diam_union' :
∀ {α : Type u} [inst : PseudoMetricSpace α] {s t : Set α},
(s ∩ t).Nonempty → Metric.diam (s ∪ t) ≤ Metric.diam s + Metric.diam t
This theorem states that in a pseudo-metric space, if two sets have a nonempty intersection, then the diameter of the union of these two sets is less than or equal to the sum of their individual diameters. The diameter of a set in this context is the greatest distance between any two points within the set. The theorem implies that the overlap between the two sets prevents the union from having a larger diameter than the sum of the individual diameters.
More concisely: In a pseudo-metric space, the diameter of the union of two sets with nonempty intersection is less than or equal to the sum of their individual diameters.
|
Metric.comap_dist_right_atTop
theorem Metric.comap_dist_right_atTop :
∀ {α : Type u} [inst : PseudoMetricSpace α] (c : α),
Filter.comap (fun x => dist x c) Filter.atTop = Bornology.cobounded α
This theorem states that for any type `α` that is a pseudometric space, and for any element `c` of type `α`, the filter obtained by the function `comap` applied to the distance function from `c` (i.e., the function that takes `x` to the distance from `x` to `c`) and the filter representing the limit towards infinity (i.e., `Filter.atTop`), is equal to the filter of cobounded sets in the bornology of `α`. In other words, mapping the distance from a fixed point `c` to each point in the space `α` under the filter going to infinity results in the filter of all sets that are bounded away from `α`.
More concisely: For any pseudometric space `α` and element `c` in `α`, the filter obtained by applying `comap` to the distance function from `c` and the filter at infinity is equal to the filter of cobounded sets in the bornology of `α`.
|
Metric.isBounded_of_bddAbove_of_bddBelow
theorem Metric.isBounded_of_bddAbove_of_bddBelow :
∀ {α : Type u} [inst : PseudoMetricSpace α] [inst_1 : Preorder α] [inst_2 : CompactIccSpace α] {s : Set α},
BddAbove s → BddBelow s → Bornology.IsBounded s
This theorem states that in a pseudo metric space, which also has a conditionally complete linear order where the order and the metric structure induce the same topology, any set that is order-bounded (that is, it has both an upper and lower bound) is also metrically bounded according to the given bornology. In the context of the theorem, a pseudo metric space is a space in which distances between points are defined and satisfy certain properties, and a bornology is a way of understanding boundedness in such spaces.
More concisely: In a pseudo metric space with a compatible linear order inducing the same topology, every order-bounded set is metrically bounded.
|
Metric.ediam_le_of_forall_dist_le
theorem Metric.ediam_le_of_forall_dist_le :
∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} {C : ℝ},
(∀ x ∈ s, ∀ y ∈ s, dist x y ≤ C) → EMetric.diam s ≤ ENNReal.ofReal C
The theorem `Metric.ediam_le_of_forall_dist_le` states that in any pseudometric space, if the distance between any two points in a set is bounded by a constant `C`, then the extended non-negative real representation of `C` (`ENNReal.ofReal C`) is an upper bound for the extended metric diameter of the set. The extended metric diameter of a set in this context is defined as the supremum of the distances between all pairs of points in the set. This theorem, therefore, provides a connection between the concepts of bounded distance and the extended metric diameter in pseudometric spaces.
More concisely: In a pseudometric space, the extended non-negative real representation of the supremum of distances between any two points in a set is an upper bound for the extended metric diameter of that set.
|
Metric.isBounded_iff_subset_closedBall
theorem Metric.isBounded_iff_subset_closedBall :
∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} (c : α),
Bornology.IsBounded s ↔ ∃ r, s ⊆ Metric.closedBall c r
This theorem states that for any given point `c` in a pseudo-metric space `α`, a subset `s` of `α` is bounded with respect to the associated bornology if and only if there exists a real number `r` such that `s` is a subset of the closed ball around `c` with radius `r`. A closed ball in this context is defined as the set of all points `y` in `α` such that the distance from `y` to `c` is less than or equal to `r`.
More concisely: A subset of a pseudo-metric space is bounded with respect to the associated bornology if and only if it is contained in the closed ball around some point with a finite radius.
|
Bornology.IsBounded.subset_closedBall
theorem Bornology.IsBounded.subset_closedBall :
∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α},
Bornology.IsBounded s → ∀ (c : α), ∃ r, s ⊆ Metric.closedBall c r
This theorem states that for any type `α` that is a pseudometric space, and for any set `s` of this type, if `s` is bounded according to the bornology of `α`, then for any chosen element `c` from `α`, there exists a real number `r` such that `s` is a subset of the closed ball centered at `c` with radius `r`. Here, a closed ball in a pseudometric space is defined as the set of all points whose distance from the center is less than or equal to the radius, and a set is said to be bounded according to the bornology if its complement is co-bounded.
More concisely: For any bounded subset `s` of a pseudometric space `α` with respect to its bornology, there exists a real number `r` such that `s` is contained in the closed ball centered at any chosen point `c` in `α` with radius `r`.
|
Metric.diam_ball
theorem Metric.diam_ball :
∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {r : ℝ}, 0 ≤ r → Metric.diam (Metric.ball x r) ≤ 2 * r := by
sorry
The theorem `Metric.diam_ball` states that, for any type `α` equipped with a pseudo metric space structure, any point `x` of type `α`, and any non-negative real number `r`, the diameter of the metric ball centered at `x` with radius `r` is less than or equal to `2r`. In slightly more mathematical terms, if we denote the set of all points `y` such that the distance between `y` and `x` is less than `r` by `Metric.ball x r` (this is a ball of radius `r` centered at `x`), then the diameter of this set (the greatest distance between any two points in the set) does not exceed `2r`.
More concisely: The diameter of a metric ball in a pseudo metric space is less than or equal to twice its radius.
|
Metric.diam_le_of_forall_dist_le_of_nonempty
theorem Metric.diam_le_of_forall_dist_le_of_nonempty :
∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α},
s.Nonempty → ∀ {C : ℝ}, (∀ x ∈ s, ∀ y ∈ s, dist x y ≤ C) → Metric.diam s ≤ C
This theorem states that in a nonempty set within a pseudometric space, if the distance between any two points in the set is bounded by some constant `C`, then `C` also bounds the diameter of the set. Here, the diameter of the set is calculated using the function `Metric.diam`, which is converted to a real number from the extended metric diameter. The pseudometric space, set, and constant `C` are all universal quantifications, meaning this theorem applies to any such entities that satisfy the conditions.
More concisely: In a nonempty set of a pseudometric space, the diameter is bounded by the supreme distance between any two points in the set.
|
Metric.diam_le_of_forall_dist_le
theorem Metric.diam_le_of_forall_dist_le :
∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} {C : ℝ},
0 ≤ C → (∀ x ∈ s, ∀ y ∈ s, dist x y ≤ C) → Metric.diam s ≤ C
This theorem states that in any pseudo-metric space, if the distance between any two points in a given set is bounded by some non-negative constant, then this constant also bounds the diameter of the set. Given a type `α` that is a pseudo-metric space, a set `s` of type `α`, and a non-negative real number `C`, if for every pair of points `x` and `y` in the set `s`, the distance between `x` and `y` is less than or equal to `C`, then the diameter of the set `s` is also less than or equal to `C`.
More concisely: In a pseudo-metric space, if the distance between any two points in a set is bounded by a constant, then that constant is an upper bound for the diameter of the set.
|
Metric.diam_eq_zero_of_unbounded
theorem Metric.diam_eq_zero_of_unbounded :
∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α}, ¬Bornology.IsBounded s → Metric.diam s = 0
This theorem states that in any pseudometric space, the diameter of an unbounded set is zero. It essentially relates the concepts of 'boundedness' and 'diameter' by asserting that if a set is not bounded (i.e., it's unbounded) then its diameter is zero. If you want the diameter to be infinity for unbounded sets, you can use `EMetric.diam` instead. The primary utility of this theorem is that it allows us to avoid additional conditions in certain situations.
More concisely: In a pseudometric space, the diameter of an unbounded set is 0.
|
Metric.diam_singleton
theorem Metric.diam_singleton : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α}, Metric.diam {x} = 0
The theorem `Metric.diam_singleton` states that for any type `α` that forms a pseudometric space (a space where the distance between two points satisfies all the properties of a metric except possibly the property that two points are identical if and only if their distance is zero), the diameter of a set containing a single element `x` is zero. In other words, in any pseudometric space, the diameter of a singleton set is always zero.
More concisely: In any pseudometric space, the diameter of a singleton set is 0.
|
Metric.isBounded_of_compactSpace
theorem Metric.isBounded_of_compactSpace :
∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} [inst_1 : CompactSpace α], Bornology.IsBounded s
The theorem `Metric.isBounded_of_compactSpace` states that in a compact space, all sets are bounded. Specifically, for any type `α` that has a pseudo-metric space structure and any set `s` of type `α`, if `α` also has a compact space structure, then `s` is bounded relative to the ambient bornology on `α`. In other words, all subsets of a compact space are bounded in the sense of bornology.
More concisely: In a compact metric space, every subset is bounded.
|
Metric.nonempty_iInter_of_nonempty_biInter
theorem Metric.nonempty_iInter_of_nonempty_biInter :
∀ {α : Type u} [inst : PseudoMetricSpace α] [inst_1 : CompleteSpace α] {s : ℕ → Set α},
(∀ (n : ℕ), IsClosed (s n)) →
(∀ (n : ℕ), Bornology.IsBounded (s n)) →
(∀ (N : ℕ), (⋂ n, ⋂ (_ : n ≤ N), s n).Nonempty) →
Filter.Tendsto (fun n => Metric.diam (s n)) Filter.atTop (nhds 0) → (⋂ n, s n).Nonempty
The theorem `Metric.nonempty_iInter_of_nonempty_biInter` states: Given a complete pseudo-metric space, if we have a sequence of closed and bounded sets such that the diameter of these sets goes to zero as we approach infinity and every finite intersection of these sets is non-empty, then the intersection of all the sets in the sequence is also non-empty. In mathematical terms, given a family ${s_n} _{n \in \mathbb{N}}$ of closed and bounded sets in a complete pseudo-metric space, if $\lim_{n \to \infty} \text{diam}(s_n) = 0$ and $\bigcap_{n=1}^N s_n \neq \emptyset$ for all $N \in \mathbb{N}$, then $\bigcap_{n=1}^\infty s_n \neq \emptyset$.
More concisely: If ${s_n}$ is a sequence of closed and bounded sets in a complete pseudo-metric space with $\lim\limits_{n \to \infty} \text{diam}(s_n) = 0$ and $\bigcap\limits_{n=1}^N s_n \neq \emptyset$ for all $N$, then $\bigcap\limits_{n=1}^\infty s_n \neq \emptyset$.
|
Metric.isCompact_of_isClosed_isBounded
theorem Metric.isCompact_of_isClosed_isBounded :
∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} [inst_1 : ProperSpace α],
IsClosed s → Bornology.IsBounded s → IsCompact s
The **Heine-Borel theorem** states that in a proper space - a space where every closed ball is compact - if a set is both closed and bounded, it is also compact. In other words, for any type `α` equipped with a pseudometric space structure and for any set `s` of type `α` in a proper space, if `s` is closed and `s` is bounded with respect to the bornology on `α` (meaning that it is not larger than any given set in the bornology), then `s` is compact. A set is compact if, for every nontrivial filter that contains the set, there exists a point in the set such that every set in the filter intersects with every neighborhood of that point.
More concisely: In a proper metric space, a bounded and closed set is compact.
|
Metric.diam_union
theorem Metric.diam_union :
∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} {x y : α} {t : Set α},
x ∈ s → y ∈ t → Metric.diam (s ∪ t) ≤ Metric.diam s + dist x y + Metric.diam t
This theorem states that in any pseudo metric space, the diameter of the union of two sets is bounded above by the sum of the diameters of the two sets and the distance between any one point in each set. This is true under all circumstances, including the case where the union of the two sets is unbounded.
More concisely: In any pseudo-metric space, the diameter of the union of two sets is less than or equal to the sum of the diameters of the sets and the distance between any two points, one in each set.
|
IsCompact.isBounded
theorem IsCompact.isBounded :
∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α}, IsCompact s → Bornology.IsBounded s
This theorem states that for any set `s` in a pseudometric space `α`, if `s` is a compact set, then it is also a bounded set. Compactness here means that for every nontrivial filter on `s`, there exists an element in `s` such that every set in the filter intersects every neighborhood of this element. Boundedness, on the other hand, is defined relative to the ambient bornology on `α`, meaning the set `s` is bounded if its complement is cobounded in this bornology.
More concisely: In a pseudometric space, every compact set is bounded.
|
Metric.cobounded_le_cocompact
theorem Metric.cobounded_le_cocompact :
∀ {α : Type u} [inst : PseudoMetricSpace α], Bornology.cobounded α ≤ Filter.cocompact α
The theorem `Metric.cobounded_le_cocompact` states that for any type `α` equipped with a pseudo metric space structure, the filter of cobounded sets in the bornology of `α` is less than or equal to the filter generated by the complements of compact sets in the topological space of `α`. In mathematical terms, this means that every cobounded set in the bornology of a pseudo metric space is also a cocompact set in the same space.
More concisely: In a pseudo metric space, the filter of cobounded sets is contained in the filter generated by the complements of compact sets.
|
Metric.closedBall_compl_subset_of_mem_cocompact
theorem Metric.closedBall_compl_subset_of_mem_cocompact :
∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α},
s ∈ Filter.cocompact α → ∀ (c : α), ∃ r, (Metric.closedBall c r)ᶜ ⊆ s
The theorem `Metric.closedBall_compl_subset_of_mem_cocompact` states that for any type `α` that forms a pseudo metric space, and for any set `s` of type `α` that belongs to the filter generated by the complements of compact sets in this space, we can state the following: For any element `c` of type `α`, there exists a real number `r` such that the complement of the closed ball around `c` with radius `r` is a subset of `s`. In other words, you can always find a closed ball around any point in such a way that everything outside this ball is in the specified set `s` from the filter of complements to compact sets.
More concisely: For any pseudo metric space `α` and set `s` generated by complements of compact sets, there exists a radius `r` such that for all `c` in `α`, the complement of the closed ball around `c` with radius `r` is contained in `s`.
|
Metric.isBounded_range_iff
theorem Metric.isBounded_range_iff :
∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] {f : β → α},
Bornology.IsBounded (Set.range f) ↔ ∃ C, ∀ (x y : β), dist (f x) (f y) ≤ C
This theorem characterizes the boundedness of the range of a function in a pseudo-metric space. It states that for any types `α` and `β`, given `α` is a pseudo-metric space and `f` is a function from `β` to `α`, the range of function `f` is bounded if and only if there exists a real number `C` such that for all `x` and `y` in `β`, the distance between `f(x)` and `f(y)` in `α` is less than or equal to `C`. In other words, the range of `f` is bounded if and only if `f` is uniformly continuous.
More concisely: A function from a pseudo-metric space to another pseudo-metric space is bounded if and only if it is uniformly continuous.
|
Metric.exists_isOpen_isBounded_image_of_isCompact_of_forall_continuousAt
theorem Metric.exists_isOpen_isBounded_image_of_isCompact_of_forall_continuousAt :
∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : TopologicalSpace β] {k : Set β} {f : β → α},
IsCompact k → (∀ x ∈ k, ContinuousAt f x) → ∃ t, k ⊆ t ∧ IsOpen t ∧ Bornology.IsBounded (f '' t)
This theorem states that, given a set `k` within a topological space `β` and a function `f` mapping `β` to a pseudo metric space `α`, if `k` is compact (meaning that for any nontrivial filter that contains `k`, there is a point in `k` where every set of the filter intersects every neighborhood of that point) and the function `f` is continuous at every point in `k` (which means that as a point in `k` gets infinitesimally close to some other point, the image of the point under `f` gets infinitesimally close to the image of the other point), then there exists an open set `t` (a set that is open in the topological space `β`) which contains `k` and the image of `t` under `f` is bounded in `α` (meaning there exists a ball in the metric space `α` that contains all images of points in `t` under `f`). In other words, we can always find some open neighborhood of a compact set on which a continuous function is bounded.
More concisely: Given a compact subset `k` of a topological space `β` and a continuous function `f` from `β` to a metric space `α`, there exists an open set `t` containing `k` such that the image of `t` under `f` is bounded in `α`.
|
Metric.diam_empty
theorem Metric.diam_empty : ∀ {α : Type u} [inst : PseudoMetricSpace α], Metric.diam ∅ = 0
The theorem `Metric.diam_empty` states that for any pseudometric space `α`, the diameter of the empty set is zero. Here, the diameter of a set in a pseudometric space is defined using the e-metric diameter function `EMetric.diam`, which is then converted to a real number using the `.toReal` function.
More concisely: In any pseudometric space, the diameter of the empty set is 0.
|
Metric.diam_closedBall
theorem Metric.diam_closedBall :
∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {r : ℝ}, 0 ≤ r → Metric.diam (Metric.closedBall x r) ≤ 2 * r
The theorem `Metric.diam_closedBall` states that in any pseudometric space, the diameter of a closed ball with radius `r` is at most `2 * r`. More specifically, for any point `x` in the pseudometric space and any non-negative real number `r`, the diameter of the set of all points `y` that are at a distance less than or equal to `r` from `x` (the `closedBall` around `x` with radius `r`) is less than or equal to `2 * r`.
More concisely: In any pseudometric space, the diameter of a closed ball centered at a point with radius r is at most 2r.
|
Metric.isBounded_closedBall
theorem Metric.isBounded_closedBall :
∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {r : ℝ}, Bornology.IsBounded (Metric.closedBall x r)
This theorem states that for any pseudometric space, given any point `x` in the space and any real number `r`, the closed ball centered at `x` with radius `r` is a bounded set. Here, a closed ball is defined as the set of all points `y` such that the distance from `y` to `x` is less than or equal to `r`. A set is considered bounded relative to the ambient bornology if its complement is cobounded.
More concisely: For any pseudometric space and point `x` in it, the closed ball centered at `x` with radius `r` is a bounded set. (A set is bounded if its complement is cobounded in the ambient topology.)
|
Metric.diam_mono
theorem Metric.diam_mono :
∀ {α : Type u} [inst : PseudoMetricSpace α] {s t : Set α},
s ⊆ t → Bornology.IsBounded t → Metric.diam s ≤ Metric.diam t
The theorem `Metric.diam_mono` states that for any type `α` which has a structure of a PseudoMetricSpace, and for any two sets `s` and `t` of elements of type `α`, if `s` is a subset of `t` and `t` is a bounded set (according to the bornology on `α`), then the diameter of the set `s` is less than or equal to the diameter of the set `t`. In other words, if we have a set within a bounded set in a pseudo-metric space, the diameter of the inner set is always bounded by the diameter of the outer set.
More concisely: In a PseudoMetricSpace, the diameter of a bounded subset is greater than or equal to the diameter of any smaller subset it contains. (Note that the original statement was incorrectly stated as the diameter of a subset being less than or equal to that of a larger bounded set.)
|
Metric.disjoint_nhds_cobounded
theorem Metric.disjoint_nhds_cobounded :
∀ {α : Type u} [inst : PseudoMetricSpace α] (x : α), Disjoint (nhds x) (Bornology.cobounded α)
The theorem `Metric.disjoint_nhds_cobounded` states that for any pseudometric space `α` and any element `x` in that space, the neighborhood filter of `x` (which contains all open sets around `x`) is disjoint from the filter of cobounded sets in the bornology of the space. In other words, there are no sets that are both a neighborhood of `x` and cobounded in the same space. Here, two sets are considered to be disjoint if their intersection (infimum in the lattice of sets) is the empty set, or equivalently, the bottom element in the lattice of sets.
More concisely: For any pseudometric space and its element, the neighborhood filter and the filter of cobounded sets are disjoint.
|
Metric.cobounded_eq_cocompact
theorem Metric.cobounded_eq_cocompact :
∀ {α : Type u} [inst : PseudoMetricSpace α] [inst_1 : ProperSpace α], Bornology.cobounded α = Filter.cocompact α
This theorem establishes the equivalence between the filter of cobounded sets in a bornology and the filter generated by the complements to compact sets in a pseudometric space that is also a proper space. More precisely, for any pseudometric space that is a proper space, the filter of sets that are not bounded away from any point in the space (the cobounded sets in the bornology of the space) is the same as the filter generated by the complements of compact subsets of the space.
More concisely: In a proper pseudometric space, the filter of cobounded sets equals the filter generated by the complements of compact sets.
|
Metric.isCompact_iff_isClosed_bounded
theorem Metric.isCompact_iff_isClosed_bounded :
∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} [inst_1 : T2Space α] [inst_2 : ProperSpace α],
IsCompact s ↔ IsClosed s ∧ Bornology.IsBounded s
The **Heine-Borel theorem** states: In a proper Hausdorff (or, equivalently, T2) space, a set is considered compact if and only if it is both closed and bounded. In more formal terms, for any type `α` in a PseudoMetricSpace, and a set `s` of type `α` in a T2Space and a ProperSpace, `s` is compact (as defined by `IsCompact`) if and only if `s` is closed (as defined by `IsClosed`) and `s` is bounded (as defined by `Bornology.IsBounded`).
More concisely: In a proper Hausdorff space, a set is compact if and only if it is both closed and bounded.
|
Metric.dist_le_diam_of_mem'
theorem Metric.dist_le_diam_of_mem' :
∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} {x y : α},
EMetric.diam s ≠ ⊤ → x ∈ s → y ∈ s → dist x y ≤ Metric.diam s
This theorem states that, in a pseudo metric space, the distance between any two points in a set is bounded by the diameter of the set. Specifically, for any set within a pseudo metric space and any two points within that set, if the diameter of the set is not infinite, then the distance between the two points is less than or equal to the diameter of the set. In mathematical terms, if `s` is a set in a pseudo metric space `α`, and `x` and `y` are elements of `s` such that the diameter of `s` is not infinity, then the distance between `x` and `y` is less than or equal to the diameter of `s`.
More concisely: In a pseudo metric space, the distance between any two points in a finite-diameter set is less than or equal to the diameter of the set.
|