Mathlib.Topology.MetricSpace.Basic._auxLemma.9
theorem Mathlib.Topology.MetricSpace.Basic._auxLemma.9 : ∀ {n m : NNReal}, (n = m) = (↑n = ↑m)
This theorem, titled `Mathlib.Topology.MetricSpace.Basic._auxLemma.9`, states that for any two non-negative real numbers `n` and `m` (represented as `NNReal` in Lean), `n` is equal to `m` if and only if their real number equivalents (obtained by applying the coercion function `↑`) are equal. This essentially indicates that the equality operation in the non-negative real numbers space (`NNReal`) is consistent with the equality operation in the real numbers space.
More concisely: For any `NNReal n` and `NNReal m`, `n = m` if and only if `↑n = ↑m`.
|
Metric.closedEmbedding_of_pairwise_le_dist
theorem Metric.closedEmbedding_of_pairwise_le_dist :
∀ {γ : Type w} [inst : MetricSpace γ] {α : Type u_3} [inst_1 : TopologicalSpace α] [inst_2 : DiscreteTopology α]
{ε : ℝ}, 0 < ε → ∀ {f : α → γ}, (Pairwise fun x y => ε ≤ dist (f x) (f y)) → ClosedEmbedding f
The theorem `Metric.closedEmbedding_of_pairwise_le_dist` states that for any type `γ` with a metric space structure, any type `α` with a topological space structure and discrete topology, any function `f` from `α` to `γ`, and any positive real number `ε`, if the distance between the images of every pair of distinct elements in `α` under `f` is at least `ε`, then `f` is a closed embedding. In other words, if every pair of distinct points in `α` map to points in `γ` that are at least `ε` apart, then `f` is a type of continuous function that preserves the closure of subsets.
More concisely: If a function from a discrete topological space to a metric space maps distinct points to points at least a fixed distance apart, then the function is a closed embedding.
|
dist_eq_zero
theorem dist_eq_zero : ∀ {γ : Type w} [inst : MetricSpace γ] {x y : γ}, dist x y = 0 ↔ x = y
This theorem states that for any type `γ` that is a metric space, the distance between two points `x` and `y` in that space is zero if and only if `x` and `y` are the same point. This is a fundamental property in metric spaces, formalizing the intuitive notion that two distinct points cannot be at zero distance from each other.
More concisely: In a metric space `γ`, points `x` and `y` have zero distance if and only if `x = y`.
|
eq_of_nndist_eq_zero
theorem eq_of_nndist_eq_zero : ∀ {γ : Type w} [inst : MetricSpace γ] {x y : γ}, nndist x y = 0 → x = y
This theorem, "eq_of_nndist_eq_zero", states that in any metric space γ, if the nonnegative distance (often called the "normed distance" or "nndist") between two points x and y is zero, then x and y are in fact the same point. This is a fundamental theorem in metric spaces, asserting that the only way for two points to have no distance between them is if they are identical.
More concisely: In any metric space, two points with zero non-negative distance are equal.
|
dist_le_zero
theorem dist_le_zero : ∀ {γ : Type w} [inst : MetricSpace γ] {x y : γ}, dist x y ≤ 0 ↔ x = y
This theorem states that for any metric space γ and any two points x and y in γ, the distance between x and y is less than or equal to 0 if and only if x and y are the same point. In other words, in any metric space, the only way for the distance between two points to be non-positive (i.e., zero or less) is if the two points are identical.
More concisely: In any metric space, the distance between two points is non-positive if and only if they are equal.
|
nndist_eq_zero
theorem nndist_eq_zero : ∀ {γ : Type w} [inst : MetricSpace γ] {x y : γ}, nndist x y = 0 ↔ x = y
This theorem, `nndist_eq_zero`, encapsulates the concept that for any two points `x` and `y` in a metric space `γ`, the nonnegative distance between them is zero if and only if the two points are identical. In other words, it characterizes the equality of points in terms of the nonnegative distance between them vanishing to zero.
More concisely: In a metric space, two points are equal if and only if their non-negative distance is zero.
|
dist_pos
theorem dist_pos : ∀ {γ : Type w} [inst : MetricSpace γ] {x y : γ}, 0 < dist x y ↔ x ≠ y
This theorem, `dist_pos`, states that for any type `γ` in a metric space, the distance between two points `x` and `y` of type `γ` is greater than 0 if and only if `x` and `y` are not equal. In other words, in any metric space, two points have positive distance between them if and only if they are distinct.
More concisely: In a metric space, the distance between two points is positive if and only if they are distinct.
|
Metric.uniformEmbedding_bot_of_pairwise_le_dist
theorem Metric.uniformEmbedding_bot_of_pairwise_le_dist :
∀ {α : Type u} [inst : PseudoMetricSpace α] {β : Type u_3} {ε : ℝ},
0 < ε → ∀ {f : β → α}, (Pairwise fun x y => ε ≤ dist (f x) (f y)) → UniformEmbedding f
The theorem `Metric.uniformEmbedding_bot_of_pairwise_le_dist` states that if we have a function `f` that maps from type `β` to type `α` in a `PseudoMetricSpace`, such that for any two distinct points in `β`, the distance between their images in `α` is at least a positive real number `ε`, then `f` is a uniform embedding with respect to the discrete uniformity on `β`. In other words, if `f` separates distinct points in `β` by at least a certain distance in `α`, it preserves the uniformity structure of `β` when mapped to `α`.
More concisely: If a function from a distinct-pointed PseudoMetricSpace to another PseudoMetricSpace with the property that the distance between any pair of distinct points is greater than a positive real number, is a uniform embedding with respect to the discrete uniformity on the domain.
|
Metric.subsingleton_closedBall
theorem Metric.subsingleton_closedBall :
∀ {γ : Type w} [inst : MetricSpace γ] (x : γ) {r : ℝ}, r ≤ 0 → (Metric.closedBall x r).Subsingleton
The theorem `Metric.subsingleton_closedBall` states that for any type `γ` that has a `MetricSpace` instance, any point `x` of type `γ`, and any real number `r`, if `r` is less than or equal to zero, then the closed ball centered at `x` with radius `r` is a `Subsingleton` set. In other words, a closed ball in a metric space with non-positive radius can contain at most one point.
More concisely: For any metric space `(γ, d)` and point `x ∈ γ` with non-positive radius `r ∈ ℝ`, the closed ball `{y ∈ γ : d(x, y) ≤ r}` contains at most one element.
|
Metric.closedBall_zero
theorem Metric.closedBall_zero : ∀ {γ : Type w} [inst : MetricSpace γ] {x : γ}, Metric.closedBall x 0 = {x}
The theorem `Metric.closedBall_zero` states that for any type `γ` equipped with a metric space structure and any element `x` of `γ`, the closed ball of radius 0 around `x` is exactly the set containing `x` alone. In other words, in any metric space, the set of all points at a distance less than or equal to 0 from a given point `x` is just the set `{x}` itself.
More concisely: In any metric space, the closed ball with radius 0 around a point is equal to the singleton set containing that point.
|
MetricSpace.ext
theorem MetricSpace.ext :
∀ {α : Type u_3} {m m' : MetricSpace α}, PseudoMetricSpace.toDist = PseudoMetricSpace.toDist → m = m'
This theorem states that if two metric space structures, `m` and `m'`, over the same type `α`, have the same distance function (as determined by the `PseudoMetricSpace.toDist` function), then these two metric space structures are equivalent, i.e., `m` equals `m'`. In other words, the distance function uniquely determines the structure of the metric space.
More concisely: If two metric space structures over the same type have the same distance function, then they are equal.
|
Metric.uniformEmbedding_iff'
theorem Metric.uniformEmbedding_iff' :
∀ {β : Type v} {γ : Type w} [inst : MetricSpace γ] [inst_1 : MetricSpace β] {f : γ → β},
UniformEmbedding f ↔
(∀ ε > 0, ∃ δ > 0, ∀ {a b : γ}, dist a b < δ → dist (f a) (f b) < ε) ∧
∀ δ > 0, ∃ ε > 0, ∀ {a b : γ}, dist (f a) (f b) < ε → dist a b < δ
The theorem states that for all types `β` and `γ`, which are metric spaces, and a function `f` that maps type `γ` to type `β`, `f` is a uniform embedding if and only if two conditions are met. The first condition is that for every positive real number `ε`, there exists a positive real number `δ` such that for every pair of elements `a` and `b` from type `γ`, if the distance between `a` and `b` is less than `δ`, the distance between `f(a)` and `f(b)` is less than `ε`. The second condition is that for every positive real number `δ`, there exists a positive real number `ε` such that for every pair of elements `a` and `b` from type `γ`, if the distance between `f(a)` and `f(b)` is less than `ε`, the distance between `a` and `b` is less than `δ`. This theorem essentially captures the bi-directionality of the distance control in uniform embeddings in metric spaces.
More concisely: A function between metric spaces is a uniform embedding if and only if for every ε > 0, there exists δ > 0 such that d(a, b) < δ implies d(f(a), f(b)) < ε, and for every δ > 0, there exists ε > 0 such that d(f(a), f(b)) < ε implies d(a, b) < δ.
|
Metric.secondCountable_of_countable_discretization
theorem Metric.secondCountable_of_countable_discretization :
∀ {α : Type u} [inst : MetricSpace α],
(∀ ε > 0, ∃ β x F, ∀ (x y : α), F x = F y → dist x y ≤ ε) → SecondCountableTopology α
This theorem states that a metric space is second countable if for any given positive real number `ε`, there exists a function `F` and countable sets `β` and `x` such that for any two elements `x` and `y` in the space, if `F(x)` equals `F(y)`, then the distance between `x` and `y` is less than or equal to `ε`. Here, being second countable is a property of topological spaces where there exists a countable base for the topology. In simpler terms, the theorem says that if you can find a way to approximate every point in a metric space using countably many pieces of information, then the space has a countable topological base.
More concisely: A metric space is second countable if there exists a countable base for its topology consisting of open balls with rational radii centered at points from a countable dense subset.
|
eq_of_dist_eq_zero
theorem eq_of_dist_eq_zero : ∀ {γ : Type w} [inst : MetricSpace γ] {x y : γ}, dist x y = 0 → x = y
This theorem is named `eq_of_dist_eq_zero` and it states that for any type `γ` which is a metric space, if the distance between two points `x` and `y` in this space is zero, then `x` and `y` must be the same point. In other words, in any metric space, two distinct points must have a non-zero distance.
More concisely: In any metric space, two distinct points have a positive distance between them.
|
Mathlib.Topology.MetricSpace.Basic._auxLemma.1
theorem Mathlib.Topology.MetricSpace.Basic._auxLemma.1 :
∀ {γ : Type w} [inst : MetricSpace γ] {x y : γ}, (dist x y = 0) = (x = y)
This theorem from the Mathlib library in Lean 4 states that for any type `γ` that is a `MetricSpace`, and for any two elements `x` and `y` of this type, the distance between `x` and `y` being zero is equivalent to `x` being equal to `y`. In other words, in any metric space, two points are the same if and only if their distance is zero.
More concisely: In any metric space, two points have zero distance if and only if they are equal.
|
dist_ne_zero
theorem dist_ne_zero : ∀ {γ : Type w} [inst : MetricSpace γ] {x y : γ}, dist x y ≠ 0 ↔ x ≠ y
This theorem states that for any type `γ` that is a metric space, the distance between two points `x` and `y` of type `γ` is not equal to zero if and only if `x` and `y` are not the same point. Essentially, in any metric space, two different points will always have a non-zero distance between them.
More concisely: In any metric space, two distinct points have positive distance.
|