edist_triangle_left
theorem edist_triangle_left :
∀ {α : Type u} [inst : PseudoEMetricSpace α] (x y z : α), edist x y ≤ edist z x + edist z y
This theorem, known as the "Triangle inequality for the extended distance", states that for any type `α` that has an associated `PseudoEMetricSpace` instance, and any three elements `x`, `y`, and `z` of this type, the extended distance between `x` and `y` is always less than or equal to the sum of the extended distances between `z` and `x`, and `z` and `y`. This is a variant of the triangle inequality, which is a fundamental property of metric spaces.
More concisely: For any type `α` with `PseudoEMetricSpace` instance and any `x, y, z` in `α`, the extended distance from `x` to `y` is less than or equal to the sum of the extended distances from `x` to `z` and `z` to `y`.
|
EMetric.diam_subsingleton
theorem EMetric.diam_subsingleton :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {s : Set α}, s.Subsingleton → EMetric.diam s = 0
The theorem `EMetric.diam_subsingleton` states that for any set `s` in a pseudoemetric space `α`, if `s` is a subsingleton set (meaning it has at most one element), then the diameter of `s` is zero. This is to say, in a pseudoemetric space, the maximum distance (or diameter) between any two points in a subsingleton set is zero, which follows naturally as there is at most one point in such a set.
More concisely: In a pseudometric space, the diameter of a subsingleton set is zero.
|
EMetric.diam_union
theorem EMetric.diam_union :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {x y : α} {s t : Set α},
x ∈ s → y ∈ t → EMetric.diam (s ∪ t) ≤ EMetric.diam s + edist x y + EMetric.diam t
The theorem `EMetric.diam_union` states that for any type `α` with a pseudoemetric space structure and any two elements `x` and `y` from `α`, along with two sets `s` and `t` of type `α`, if `x` belongs to `s` and `y` belongs to `t`, then the diameter (i.e., the greatest distance between any two points) of the union of `s` and `t` is less than or equal to the sum of the diameter of `s`, the edistance (extended distance, which can take the value ∞) between `x` and `y`, and the diameter of `t`. In mathematical terms, if $x \in s$ and $y \in t$, then $diam(s \cup t) \leq diam(s) + d(x, y) + diam(t)$.
More concisely: For any pseudometric space (α, d), and sets s, t ∈ α with x ∈ s and y ∈ t, the diameter of their union is bounded by the sum of the diameters of s, x and y's extended distance, and t. In other words, diam(s ∪ t) ≤ diam(s) + d(x, y) + diam(t).
|
Mathlib.Topology.EMetricSpace.Basic._auxLemma.5
theorem Mathlib.Topology.EMetricSpace.Basic._auxLemma.5 : ∀ {α : Type u} (x : α), (x ∈ Set.univ) = True
This theorem, named as `Mathlib.Topology.EMetricSpace.Basic._auxLemma.5`, states that for any type `α` and any element `x` of this type, `x` belongs to the universal set `Set.univ` of type `α`. In more mathematical terms, we could say that for any set `α` and any element `x` in `α`, the membership of `x` in the universal set corresponding to `α` is a true statement. This is consistent with the concept of a universal set, which, by definition, contains all elements of a given type or set.
More concisely: For any type `α` and any element `x` of type `α`, `x` is an element of the universal set `Set.univ` of type `α`.
|
edist_pi_le_iff
theorem edist_pi_le_iff :
∀ {β : Type v} {π : β → Type u_2} [inst : Fintype β] [inst_1 : (b : β) → EDist (π b)] {f g : (b : β) → π b}
{d : ENNReal}, edist f g ≤ d ↔ ∀ (b : β), edist (f b) (g b) ≤ d
The theorem `edist_pi_le_iff` states that for all types `β` and `π` functions from `β` to `π`, given the condition that `β` is a finite type and for all `b` in `β` there is an extended distance `EDist` on `π b`, for any two functions `f` and `g` from `β` to `π b` and an extended nonnegative real number `d`, the extended distance between `f` and `g` is less than or equal to `d` if and only if the extended distance between `f b` and `g b` for all `b` in `β` is less than or equal to `d`. In other words, the extended distance between the two functions `f` and `g` is bounded by `d` if and only if the extended distance between each of the corresponding elements they produce is also bounded by `d` for all elements in `β`.
More concisely: For functions `f` and `g` from a finite type `β` to a type `π` equipped with an extended distance, `EDist`, the extended distance between `f` and `g` is less than or equal to a given extended nonnegative real number `d` if and only if the extended distance between `f(b)` and `g(b)` is less than or equal to `d` for all `b` in `β`.
|
EMetric.edist_le_diam_of_mem
theorem EMetric.edist_le_diam_of_mem :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {x y : α} {s : Set α}, x ∈ s → y ∈ s → edist x y ≤ EMetric.diam s := by
sorry
The theorem `EMetric.edist_le_diam_of_mem` states that in a pseudoemetric space, for any given set and any two points within that set, the extended distance (or edistance) between these two points is always less than or equal to the diameter of the set. In other words, the maximum possible distance between any two points in a set can never be exceeded by the distance between any specific pair of points within that same set. This is a fundamental property of distances in general metric and pseudoemetric spaces.
More concisely: In a pseudometric space, the edistance between any two points in a set is less than or equal to the diameter of that set.
|
edist_le_range_sum_edist
theorem edist_le_range_sum_edist :
∀ {α : Type u} [inst : PseudoEMetricSpace α] (f : ℕ → α) (n : ℕ),
edist (f 0) (f n) ≤ (Finset.range n).sum fun i => edist (f i) (f (i + 1))
The theorem `edist_le_range_sum_edist` states that for any sequence of points `f : ℕ → α` in a pseudoemetric space `α` and for any natural number `n`, the extended distance (often denoted as `edist`) between the first point `f 0` and the `n`-th point `f n` is less than or equal to the sum of the extended distances between each consecutive pair of points in the range from `0` to `n-1`. In other words, the direct path between two points in the sequence is never longer than the path obtained by summing up the distances between all intermediate points, which is a variant of the triangle inequality for sequences of points.
More concisely: For any sequence of points in a pseudometric space and natural number, the extended distance between the first and last points is less than or equal to the sum of extended distances between consecutive pairs.
|
edist_le_Ico_sum_of_edist_le
theorem edist_le_Ico_sum_of_edist_le :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {f : ℕ → α} {m n : ℕ},
m ≤ n →
∀ {d : ℕ → ENNReal},
(∀ {k : ℕ}, m ≤ k → k < n → edist (f k) (f (k + 1)) ≤ d k) →
edist (f m) (f n) ≤ (Finset.Ico m n).sum fun i => d i
This theorem, named `edist_le_Ico_sum_of_edist_le`, is a version of `edist_le_Ico_sum_edist` where each intermediate distance is replaced with an upper estimate. In more specific terms, it states that for any type `α` that forms a pseudometric space, and any function `f` from natural numbers to `α`, for any natural numbers `m` and `n` such that `m` is less than or equal to `n`, and any function `d` from natural numbers to the extended non-negative real numbers (ENNReal), if for all `k` (which is a natural number) between `m` and `n` the distance in the pseudometric space between `f(k)` and `f(k+1)` is less than or equal to `d(k)`, then the distance between `f(m)` and `f(n)` is less than or equal to the sum of the values of `d(i)` for each `i` in the finite integer interval from `m` to `n`.
More concisely: For any pseudometric space (α, d), function f : ℕ → α, and function d' : ℕ → ∣∣Real.enn║∣∣, if for all i in the range from m to n, the distance d(i) between f(i) and f(i+1) is less than or equal to d'(i), then the distance from f(m) to f(n) is less than or equal to the sum of d'(i) for i from m to n.
|
EMetric.mem_closure_iff
theorem EMetric.mem_closure_iff :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {s : Set α}, x ∈ closure s ↔ ∀ ε > 0, ∃ y ∈ s, edist x y < ε
This theorem provides an ε-characterization of the closure in pseudoemetric spaces. Specifically, it states that for any type `α` that has the structure of a pseudoemetric space, for any point `x` of type `α` and any set `s` of type `α`, `x` is in the closure of `s` if and only if, for every real number `ε` greater than 0, there exists a point `y` in `s` such that the extended distance (or edistance, `edist`) between `x` and `y` is less than `ε`. In other words, `x` is in the closure of `s` if it is arbitrarily close to `s`, measured in terms of the pseudoemetric's extended distance.
More concisely: A point `x` in a pseudometric space `α` belongs to the closure of a set `s` if and only if for every `ε > 0`, there exists `y` in `s` with `edist(x, y) < ε`.
|
uniformity_dist_of_mem_uniformity
theorem uniformity_dist_of_mem_uniformity :
∀ {α : Type u} {β : Type v} [inst : LinearOrder β] {U : Filter (α × α)} (z : β) (D : α → α → β),
(∀ (s : Set (α × α)), s ∈ U ↔ ∃ ε > z, ∀ {a b : α}, D a b < ε → (a, b) ∈ s) →
U = ⨅ ε, ⨅ (_ : ε > z), Filter.principal {p | D p.1 p.2 < ε}
This theorem, `uniformity_dist_of_mem_uniformity`, characterizes the uniformities associated to a generalized distance function `D` in terms of the elements of the uniformity. It states that for any types `α` and `β`, where `β` is a linear order, and for any filter `U` on the product `α × α`, along with a given value `z` of type `β` and a distance function `D` mapping pairs of elements of `α` to `β`, if for every set `s` of pairs of `α`, `s` is in `U` if and only if there exists a `ε` greater than `z` such that for all pairs `(a, b)` of `α`, if `D(a, b)` is less than `ε` then `(a, b)` belongs to `s`, then `U` is equal to the infimum over all `ε` greater than `z` of the principal filter of the set of pairs `(p.1, p.2)` such that `D(p.1, p.2)` is less than `ε`. This theorem thus relates the structure of the filter `U` with the properties of the distance function `D`.
More concisely: Given a filter U on the product α × α, a linear order β, a value z in β, and a distance function D from α to β, U is the infimum over all ε > z of the principal filters of pairs (p.1, p.2) with D(p.1, p.2) < ε if and only if for every set s of pairs of α, s is in U if and only if there exists an ε > z such that for all (a, b) in α × α with D(a, b) < ε, (a, b) is in s.
|
EMetric.cauchySeq_iff
theorem EMetric.cauchySeq_iff :
∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : Nonempty β] [inst_2 : SemilatticeSup β]
{u : β → α}, CauchySeq u ↔ ∀ ε > 0, ∃ N, ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (u m) (u n) < ε
The theorem `EMetric.cauchySeq_iff` states that in a pseudoemetric space, a sequence is Cauchy if and only if, for any given positive real number epsilon (ε), there exists a point in the sequence such that from that point onwards, the pseudoedistance between any two points in the sequence is less than epsilon. This implies that as we progress along the sequence, the distance between the terms gets arbitrarily small. The theorem is generalized to any arbitrary type `α` that is equipped with a pseudoemetric space structure and any arbitrary type `β` that is nonempty and has a semilattice structure. The sequence is represented as a function `u` from `β` to `α`.
More concisely: In a pseudometric space, a sequence is Cauchy if and only if for any ε > 0, there exists an index such that the pseudoedistance between the sequence's terms at that index and any later index is less than ε.
|
EMetric.ball_mem_nhds
theorem EMetric.ball_mem_nhds :
∀ {α : Type u} [inst : PseudoEMetricSpace α] (x : α) {ε : ENNReal}, 0 < ε → EMetric.ball x ε ∈ nhds x
The theorem `EMetric.ball_mem_nhds` asserts that for any type `α` which has a pseudo extended metric space structure and for any instance `x` of that type, given an extended nonnegative real number `ε` which is greater than zero, the epsilon-ball around `x` (the set of all points `y` in `α` such that the extended distance between `y` and `x` is less than `ε`) is a member of the neighborhood filter of `x`. In simpler terms, if you take any point in a pseudo extended metric space and any non-zero positive extended real number, the epsilon-ball around that point is a neighborhood of that point.
More concisely: For any pseudo extended metric space `(α, d)` and point `x ∈ α`, the epsilon-ball `{y ∈ α | d(x, y) < ε}` is an element of the neighborhood filter of `x`, for any extended non-negative real number `ε > 0`.
|
EMetric.nhds_basis_eball
theorem EMetric.nhds_basis_eball :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α}, (nhds x).HasBasis (fun ε => 0 < ε) (EMetric.ball x) := by
sorry
This theorem states that for every point `x` in a given pseudo e-metric space `α`, the neighborhood filter at `x` has a basis where each basis element is the e-metric ball around `x` with radius `ε` for all `ε` greater than 0. In other words, every neighborhood of `x` can be produced by taking unions of these e-metric balls of positive radius centered at `x`.
More concisely: For every point `x` in a pseudo-metric space `α`, the neighborhood filter at `x` is generated by the e-metric balls with positive radius centered at `x`.
|
EMetric.cauchy_iff
theorem EMetric.cauchy_iff :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {f : Filter α},
Cauchy f ↔ f ≠ ⊥ ∧ ∀ ε > 0, ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, edist x y < ε
This theorem provides an ε-δ characterization of Cauchy sequences in the context of pseudoemetric spaces. Specifically, for any type `α` equipped with a pseudoemetric space structure and any filter `f` on `α`, the filter `f` is Cauchy if and only if two conditions are met:
1. The filter `f` is not the bottom filter (i.e., it is not the filter that contains all subsets of `α`),
2. For any positive real number `ε`, there exists a set `t` in the filter `f` such that for all elements `x` and `y` in `t`, the extended distance between `x` and `y` is less than `ε`.
In other words, a filter `f` is Cauchy if it is non-trivial and any two elements in a set from `f` can be made arbitrarily close to each other.
More concisely: A filter on a pseudometric space is Cauchy if and only if it is non-trivial and any two of its elements have an extended distance less than any given positive real number.
|
EMetric.mk_uniformity_basis
theorem EMetric.mk_uniformity_basis :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {β : Type u_2} {p : β → Prop} {f : β → ENNReal},
(∀ (x : β), p x → 0 < f x) →
(∀ (ε : ENNReal), 0 < ε → ∃ x, p x ∧ f x ≤ ε) → (uniformity α).HasBasis p fun x => {p | edist p.1 p.2 < f x}
This theorem states that for any pseudo-emetric space `α` and any function `f: β → [0, ∞]`, if `f` maps the set of elements `{i | p i}` to a set of positive numbers that accumulate to zero, then the collection of `f i`-neighborhoods of the diagonal forms a basis for the uniformity of `α`. In other words, given any positive extended non-negative real number `ε`, there exists an `x` such that `p x` holds and `f x` is less than or equal to `ε`, and for these `x`, we can find a neighborhood with elements `{p | edist p.1 p.2 < f x}` that will constitute a basis for the uniform structure on `α`.
More concisely: Given any pseudo-metric space `α` and a function `f: β → [0, ∞]` such that the set of elements `{i | p i}` maps to positive accumulating numbers, the collection of `f i`-neighborhoods of the diagonal forms a basis for the uniformity of `α`.
|
uniformity_basis_edist
theorem uniformity_basis_edist :
∀ {α : Type u} [inst : PseudoEMetricSpace α],
(uniformity α).HasBasis (fun ε => 0 < ε) fun ε => {p | edist p.1 p.2 < ε}
This theorem, `uniformity_basis_edist`, states that for any type `α` which has an instance of a `PseudoEMetricSpace`, the uniformity (which is a filter on `α × α` inferred from an ambient UniformSpace structure on `α`) has a basis that is indexed by positive real numbers (`ε` such that `0 < ε`). The basis elements are the sets of all pairs `(p.1, p.2)` of elements in `α` such that the extended distance between `p.1` and `p.2` is less than `ε`. In other words, the uniformity's basis is composed of the balls of radius `ε` in the pseudoemetric space.
More concisely: For any type `α` with a `PseudoEMetricSpace` instance, the basis of its uniformity consists of all balls of radius `ε` in the pseudo-metric space, where `ε` ranges over positive real numbers.
|
edist_le_zero
theorem edist_le_zero : ∀ {γ : Type w} [inst : EMetricSpace γ] {x y : γ}, edist x y ≤ 0 ↔ x = y
This theorem states that for any given type `γ` that is an instance of an extended metric space, the extended distance (`edist`) between any two points `x` and `y` of type `γ` is less than or equal to zero if and only if `x` and `y` are the same point. This is a characterization of the non-negativity property of distances in metric spaces.
More concisely: For any extended metric space `γ`, the extended distance `edist` between points `x` and `y` of type `γ` is non-negative and equals zero if and only if `x` and `y` are equal.
|
edist_le_pi_edist
theorem edist_le_pi_edist :
∀ {β : Type v} {π : β → Type u_2} [inst : Fintype β] [inst_1 : (b : β) → EDist (π b)] (f g : (b : β) → π b) (b : β),
edist (f b) (g b) ≤ edist f g
This theorem states that for any type `β` with a finite number of elements (`Fintype β`), and any function `π` from `β` to some other type `u_2`, given two functions `f` and `g` from `β` to `π b` and any element `b` of `β`, the extended distance (`edist`) between `f b` and `g b` is always less than or equal to the extended distance between `f` and `g`. Here, we assume that there is an extended distance (`EDist`) defined for each `b` in `β`. The extended distance is a generalization of distance that is valid for all pairs of points, including possibly infinite distances.
More concisely: For any type `β` with a finite number of elements, and functions `f`, `g` : `β` -> `u_2`, and `π` : `β` -> `u_2`, and for any element `b` in `β`, the extended distance `edist (f b) (g b)` is less than or equal to `EDist f g`.
|
TopologicalSpace.IsSeparable.separableSpace
theorem TopologicalSpace.IsSeparable.separableSpace :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {s : Set α},
TopologicalSpace.IsSeparable s → TopologicalSpace.SeparableSpace ↑s
This theorem states that if a set `s` is separable in the context of topology, then the corresponding subset type is also separable in a pseudo extended metric space. The term "separable" in this context means that the set `s` is contained in the closure of a countable set. It's important to note that this doesn't necessarily mean that the countable set is contained within `s`. The proof of this theorem is not provided here.
More concisely: If a set `s` is separable in the context of topology, then its corresponding subset type is separable in a pseudo extended metric space.
|
EMetric.uniformContinuous_iff
theorem EMetric.uniformContinuous_iff :
∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β},
UniformContinuous f ↔ ∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, edist a b < δ → edist (f a) (f b) < ε
This theorem provides an epsilon-delta characterization of uniform continuity for pseudoemetric spaces. For any types `α` and `β` that are pseudoemetric spaces and any function `f` from `α` to `β`, `f` is uniformly continuous if and only if for every `ε` greater than zero, there exists a `δ` greater than zero such that for all `a` and `b` in `α`, if the pseudoemetric distance between `a` and `b` is less than `δ`, then the pseudoemetric distance between `f(a)` and `f(b)` is less than `ε`. This essentially states that if any two points are sufficiently close in the domain space, their images under the function `f` will be sufficiently close in the co-domain space.
More concisely: A function between two pseudometric spaces is uniformly continuous if and only if for every ε > 0, there exists δ > 0 such that the pseudometric distances d(a, b) < δ implies d(f(a), f(b)) < ε for all a, b in the domain.
|
eq_of_forall_edist_le
theorem eq_of_forall_edist_le : ∀ {γ : Type w} [inst : EMetricSpace γ] {x y : γ}, (∀ ε > 0, edist x y ≤ ε) → x = y := by
sorry
This theorem states that in any extended metric space, if the extended distance (`edist`) between two points `x` and `y` is less than or equal to `ε` for all positive `ε`, then the two points `x` and `y` are the same. That is, if for all positive `ε`, `x` and `y` are never more than `ε` apart, then `x` and `y` must coincide.
More concisely: In an extended metric space, if the extended distance between two points is less than or equal to every positive epsilon, then the two points are equal.
|
EMetric.mem_closedBall
theorem EMetric.mem_closedBall :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {x y : α} {ε : ENNReal}, y ∈ EMetric.closedBall x ε ↔ edist y x ≤ ε
This theorem states that for any type `α` equipped with a pseudo extended metric space structure, and for any elements `x`, `y` of type `α` and `ε` of type `ENNReal` (the extended nonnegative real numbers), `y` belongs to the closed ball centered at `x` with radius `ε` (as defined in pseudo extended metric space) if and only if the extended distance from `y` to `x` is less than or equal to `ε`. This essentially defines the property of the closed ball in the pseudo extended metric space context.
More concisely: For any pseudo extended metric space `(α, d)`, and for all `x : α`, `y : α`, and `ε : ENNReal`, `y` is in the closed ball `{z : α | d(x, z) ≤ ε}` if and only if `d(x, y) ≤ ε`.
|
EMetric.tendstoUniformly_iff
theorem EMetric.tendstoUniformly_iff :
∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] {ι : Type u_2} {F : ι → β → α} {f : β → α} {p : Filter ι},
TendstoUniformly F f p ↔ ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ (x : β), edist (f x) (F n x) < ε
The theorem `EMetric.tendstoUniformly_iff` provides a characterization of uniform convergence using the concept of extended distance (`edist`). Specifically, it states that a sequence of functions `F` (indexed by `ι`) converges uniformly to a limiting function `f` with respect to a filter `p` if and only if for any positive ε, we can find an index (according to the filter `p`) such that the extended distance between the function value `f(x)` and `(F n)(x)` is less than ε, for all `x` in the domain `β`. This condition needs to hold for all ε greater than 0, and is a way of saying that the functions in sequence `F` get arbitrarily close to `f` uniformly across all `x`.
More concisely: A sequence of functions converges uniformly to a limit with respect to a filter if and only if for every ε > 0, there exists an index according to the filter such that the extended distance between the limit and the function value at any x is less than ε.
|
edist_triangle4
theorem edist_triangle4 :
∀ {α : Type u} [inst : PseudoEMetricSpace α] (x y z t : α), edist x t ≤ edist x y + edist y z + edist z t := by
sorry
This theorem, `edist_triangle4`, states that for any type `α` that is an instance of `PseudoEMetricSpace` (a structure denoting a set equipped with an extended distance function that satisfies certain properties), and for any four elements `x`, `y`, `z`, and `t` of this type, the extended distance between `x` and `t` is always less than or equal to the sum of the extended distances between `x` and `y`, `y` and `z`, and `z` and `t`. This is a generalization of the triangle inequality in the context of pseudo extended metric spaces.
More concisely: For any pseudo-metric space `(α, d)`, and any elements `x, y, z, t` in `α`, the extended distance `d(x, t)` is less than or equal to the sum of the extended distances `d(x, y)`, `d(y, z)`, and `d(z, t)`.
|
edist_le_Ico_sum_edist
theorem edist_le_Ico_sum_edist :
∀ {α : Type u} [inst : PseudoEMetricSpace α] (f : ℕ → α) {m n : ℕ},
m ≤ n → edist (f m) (f n) ≤ (Finset.Ico m n).sum fun i => edist (f i) (f (i + 1))
This theorem, named `edist_le_Ico_sum_edist`, states the version of the triangle (polygon) inequality for sequences of points in a pseudoemetric space, specifically for the interval from `m` to `n` represented as a finite set `Finset.Ico m n`. Given a sequence `f` from natural numbers to a pseudoemetric space, and provided `m` is less than or equal to `n`, the extended distance `edist` between the `m`-th and `n`-th elements of the sequence is less than or equal to the sum of the extended distances between consecutive elements from the `m`-th to the `n`-th element. Here, the sum is taken over the finite set of natural numbers from `m` to `n-1`.
More concisely: For any sequence `f` of points in a pseudometric space and finite set `I = {m + 1, ..., n}`, the extended distance between the `m`-th and `n`-th elements `edist(f(m), f(n))` is less than or equal to the sum of extended distances between consecutive elements `edist(f(i), f(i+1))` for all `i` in `I`.
|
EMetric.controlled_of_uniformEmbedding
theorem EMetric.controlled_of_uniformEmbedding :
∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β},
UniformEmbedding f →
(∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, edist a b < δ → edist (f a) (f b) < ε) ∧
∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, edist (f a) (f b) < ε → edist a b < δ
The theorem `EMetric.controlled_of_uniformEmbedding` states that if a function `f` is a uniform embedding between two pseudoemetric spaces `α` and `β`, then the extended distance (or `edist`) between `f(x)` and `f(y)` is controlled by the distance between `x` and `y`. In other words, for any positive `ε`, there exists a positive `δ` such that, for any two points `a` and `b` in `α`, if the distance between `a` and `b` is less than `δ`, then the distance between `f(a)` and `f(b)` is less than `ε`. The theorem also states the converse: for any positive `δ`, there exists a positive `ε` such that, for any two points `a` and `b` in `α`, if the distance between `f(a)` and `f(b)` is less than `ε`, then the distance between `a` and `b` is less than `δ`.
More concisely: If `f` is a uniform embedding between pseudometric spaces `α` and `β`, then for any positive `ε`, there exists a positive `δ` such that `edist(f(x), f(y)) < ε` implies `dist(x, y) < δ` and vice versa.
|
EMetric.diam_le
theorem EMetric.diam_le :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {s : Set α} {d : ENNReal},
(∀ x ∈ s, ∀ y ∈ s, edist x y ≤ d) → EMetric.diam s ≤ d
This theorem states that for any given set `s` in a pseudo emetric space `α`, if the distance between any two points in this set is less than or equal to a certain non-negative real number `d` (possibly extended with positive infinity), then the diameter of the set `s` is also less than or equal to `d`. In other words, if every pair of points in the set is no further apart than `d`, then the greatest possible distance between any two points in the set (the diameter) is no greater than `d`.
More concisely: In a pseudometric space, the diameter of a set is less than or equal to the greatest distance between any two of its points.
|
Mathlib.Topology.EMetricSpace.Basic._auxLemma.6
theorem Mathlib.Topology.EMetricSpace.Basic._auxLemma.6 : ∀ {b : Prop} (α : Sort u_1) [i : Nonempty α], (α → b) = b
This theorem, `Mathlib.Topology.EMetricSpace.Basic._auxLemma.6`, states that for any proposition `b` and any nonempty type `α`, the function type from `α` to `b` is equivalent to `b`. In other words, if we have a function that outputs a proposition `b` for every element in a nonempty type `α`, this is the same as just having the proposition `b` itself.
More concisely: For any nonempty type `α` and proposition `b`, the function type `α → b` is equivalent to `b`.
|
EMetric.cauchySeq_iff_NNReal
theorem EMetric.cauchySeq_iff_NNReal :
∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : Nonempty β] [inst_2 : SemilatticeSup β]
{u : β → α}, CauchySeq u ↔ ∀ (ε : NNReal), 0 < ε → ∃ N, ∀ (n : β), N ≤ n → edist (u n) (u N) < ↑ε
The theorem `EMetric.cauchySeq_iff_NNReal` states that for any sequence `u` from a type `β` to a pseudo emetric space `α`, the sequence is a Cauchy sequence if and only if for every positive nonnegative real number `ε`, there exists an element `N` in `β` such that for all elements `n` in `β` greater than or equal to `N`, the extended distance between `u(n)` and `u(N)` is less than `ε`. This is a variation of the emetric characterization of Cauchy sequences that deals with nonnegative real number upper bounds.
More concisely: A sequence in a pseudo metric space is Cauchy if and only if for every positive real number ε, there exists an index N such that the extended distance between sequence elements u(N) and u(n) is less than ε for all n ≥ N.
|
EMetric.ball_subset_closedBall
theorem EMetric.ball_subset_closedBall :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {ε : ENNReal}, EMetric.ball x ε ⊆ EMetric.closedBall x ε := by
sorry
The theorem `EMetric.ball_subset_closedBall` states that for any type `α` that is a pseudo extended metric space, and for any point `x` of type `α` and extended nonnegative real number `ε`, the set of all points `y` such that the extended distance between `y` and `x` is less than `ε` (denoted as `EMetric.ball x ε`) is a subset of the set of all points `y` such that the extended distance between `y` and `x` is less than or equal to `ε` (denoted as `EMetric.closedBall x ε`). In other words, every point in the open ball (with radius `ε`) is also contained in the closed ball (with the same radius `ε`).
More concisely: For any pseudo extended metric space (α), and points x : α and y : α, if the extended distance d(x, y) < ε, then y is in the closed ball B.closedBall x ε = {z : α | d(x, z) ≤ ε}.
|
EMetric.complete_of_cauchySeq_tendsto
theorem EMetric.complete_of_cauchySeq_tendsto :
∀ {α : Type u} [inst : PseudoEMetricSpace α],
(∀ (u : ℕ → α), CauchySeq u → ∃ a, Filter.Tendsto u Filter.atTop (nhds a)) → CompleteSpace α
This theorem states that a pseudoemetric space is complete if every Cauchy sequence in it has a limit. More precisely, given a pseudoemetric space `α`, if for every sequence `u` of elements in `α` that forms a Cauchy sequence, there exists an element `a` in `α` such that `u` tends to `a` at infinity (i.e., as the sequence index goes to infinity, the sequence values get arbitrarily close to `a`), then the pseudoemetric space is complete. Here, completeness of a space is defined as the property that every Cauchy sequence in the space converges to a limit within the space.
More concisely: A pseudometric space is complete if every Cauchy sequence in it converges to a limit within the space.
|
Mathlib.Topology.EMetricSpace.Basic._auxLemma.15
theorem Mathlib.Topology.EMetricSpace.Basic._auxLemma.15 : ∀ (p : Prop), (True ∧ p) = p
This theorem, from the Mathlib.Topology.EMetricSpace.Basic, states that for any proposition 'p', the logical conjunction of 'True' and 'p' is equivalent to 'p' itself. In other words, 'p' and 'True' logically 'and'ed together will result in 'p', reflecting the logical identity that 'True' is the identity element for logical conjunction.
More concisely: The theorem asserts that for all propositions p, p and True are logically equivalent.
|
edist_mem_uniformity
theorem edist_mem_uniformity :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {ε : ENNReal}, 0 < ε → {p | edist p.1 p.2 < ε} ∈ uniformity α := by
sorry
This theorem, titled "edist_mem_uniformity", asserts that for any type `α` that is a PseudoEMetricSpace (a type of metric space that might include infinite distances), and for any extended nonnegative real number `ε` that is greater than zero, the set of all pairs `p` such that the extended distance between the two elements of `p` is less than `ε`, is a member of the uniformity of `α`. A uniformity is a structure that encapsulates the concept of being "uniformly close" in a uniform space, and in this case, it's saying that such pairs are close in the sense defined by the uniform structure of this space. This is a fundamental property in the study of metric and topological spaces.
More concisely: For any PseudoEMetricSpace α and ε > 0, the set of pairs p with edist α p < ε is a uniformity open subset of α.
|
EMetric.ball_subset_ball
theorem EMetric.ball_subset_ball :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {ε₁ ε₂ : ENNReal},
ε₁ ≤ ε₂ → EMetric.ball x ε₁ ⊆ EMetric.ball x ε₂
This theorem states that for any pseudo emetric space (a type of metric space where the distance between two points can be infinite), any point 'x' in that space, and any two extended nonnegative real numbers 'ε₁' and 'ε₂', if 'ε₁' is less than or equal to 'ε₂', then the ε-metric ball surrounding 'x' with radius 'ε₁' is a subset of the ε-metric ball surrounding 'x' with radius 'ε₂'. In simpler terms, a smaller or equal-sized sphere is always contained within a larger sphere when both spheres have the same center. The ε-metric ball is a set of all points 'y' such that the extended distance between 'y' and 'x' is less than 'ε', where 'ε' can be any nonnegative real number including infinity.
More concisely: For any pseudo-metric space and any point x, if B(x, ε₁) is the ε₁-ball and B(x, ε₂) is the ε₂-ball with the same center x, then B(x, ε₁) ⊆ B(x, ε₂) when ε₁ ≤ ε₂.
|
EMetric.diam_le_iff
theorem EMetric.diam_le_iff :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {s : Set α} {d : ENNReal},
EMetric.diam s ≤ d ↔ ∀ x ∈ s, ∀ y ∈ s, edist x y ≤ d
This theorem states that for all pseudoemetric spaces (`α`), and for any set (`s`) of elements of type `α`, and any extended non-negative real number (`d`), the diameter of the set `s` is less than or equal to `d` if and only if for every pair of elements `x` and `y` in `s`, the extended distance (`edist`) between `x` and `y` is less than or equal to `d`. In simpler terms, the diameter of a set in a pseudoemetric space is never greater than the distance between any two of its points.
More concisely: In a pseudometric space, the diameter of a set is less than or equal to the greatest distance between any two of its elements.
|
uniformity_edist
theorem uniformity_edist :
∀ {γ : Type w} [inst : EMetricSpace γ],
uniformity γ = ⨅ ε, ⨅ (_ : ε > 0), Filter.principal {p | edist p.1 p.2 < ε}
This theorem states that the uniformity (a concept from uniform spaces) of a type γ, which is equipped with an extended metric space structure, can be expressed in terms of the extended distance between elements. Concretely, the uniformity on this metric space is equal to the infimum over all positive ε of the principal filter of the set of all pairs of points in γ whose extended distance is less than ε. This gives an alternative characterization of the uniform structure for metric spaces in terms of distances.
More concisely: The uniformity of a metric space's type γ is equal to the infimum over all positive ε of the principal filter generated by the set of pairwise distances less than ε.
|
TopologicalSpace.IsSeparable.exists_countable_dense_subset
theorem TopologicalSpace.IsSeparable.exists_countable_dense_subset :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {s : Set α},
TopologicalSpace.IsSeparable s → ∃ t ⊆ s, t.Countable ∧ s ⊆ closure t
This theorem states that if a set `s` is separable in a pseudo extended metric space, then it must have a countable dense subset. This is not immediately clear, as the definition of separability provides a countable set whose closure covers `s`, but does not necessarily require that this countable set is a subset of `s`. Formally, for any set `s` in type `α` that is a pseudo extended metric space, if `s` is separable, then there exists a set `t` that is both a subset of `s` and countable, and the closure of `t` is a superset of `s`.
More concisely: If a pseudo extended metric space `s` is separable, then it has a countable dense subset.
|
EMetric.tendstoLocallyUniformly_iff
theorem EMetric.tendstoLocallyUniformly_iff :
∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] {ι : Type u_2} [inst_1 : TopologicalSpace β]
{F : ι → β → α} {f : β → α} {p : Filter ι},
TendstoLocallyUniformly F f p ↔
∀ ε > 0, ∀ (x : β), ∃ t ∈ nhds x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, edist (f y) (F n y) < ε
This theorem states that for any types `α`, `β`, and `ι` where `α` is a pseudo emetric space and `β` is a topological space, a sequence of functions `F` indexed by `ι` converges locally uniformly to a function `f` with respect to a filter `p` if and only if, for any `ε` greater than 0 and any point `x` in `β`, there exists a neighborhood `t` of `x` such that, eventually in the filter `p`, for all points `y` in `t`, the extended distance between `f(y)` and `F(n,y)` is less than `ε`.
In other words, the sequence of functions `F` converges to `f` in such a way that, around any point, the values of `F` get arbitrarily close to the value of `f` uniformly (i.e., at the same speed) across the neighborhood.
More concisely: A sequence of functions `F:` ι -> α -> β converges locally uniformly to a function `f:` β -> α with respect to a filter `p` if for every `ε>0` and `x` in β, there exists a neighborhood `t` of `x` such that, eventually in the filter `p`, for all `y` in `t`, the extended distance `d(f(y), F(i, y)) < ε` for all `i` in ι.
|
EMetric.subset_countable_closure_of_almost_dense_set
theorem EMetric.subset_countable_closure_of_almost_dense_set :
∀ {α : Type u} [inst : PseudoEMetricSpace α] (s : Set α),
(∀ ε > 0, ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, EMetric.closedBall x ε) → ∃ t ⊆ s, t.Countable ∧ s ⊆ closure t
The theorem `EMetric.subset_countable_closure_of_almost_dense_set` states that for a set `s` in a pseudo emetric space, if for every positive real number `ε`, there exists a countable set which is `ε`-dense in `s` (i.e., `s` is a subset of the union of `ε`-closed balls centered at each point in the countable set), then there exists a countable subset `t` of `s` which is dense in `s` (i.e., `s` is a subset of the closure of `t`). Here, the closure of a set is the smallest closed set containing the original set, and a set is `ε`-dense in another set if the latter set is contained within the union of `ε`-closed balls centered at each point in the former set.
More concisely: If a subset of a pseudometric space is ε-dense with a countable set for every ε, then it is a subsets of the closure of a countable dense set.
|
EMetric.diam_singleton
theorem EMetric.diam_singleton : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α}, EMetric.diam {x} = 0
The theorem `EMetric.diam_singleton` states that in any pseudoemetric space, the diameter of a singleton set (a set containing only one element) always equals zero. In other words, for any type `α` and element `x` of `α`, when `α` is considered as a pseudoemetric space, the diameter of the set containing only `x` is zero.
More concisely: In any pseudometric space, the diameter of a singleton set is 0.
|
EMetric.uniformEmbedding_iff'
theorem EMetric.uniformEmbedding_iff' :
∀ {β : Type v} {γ : Type w} [inst : EMetricSpace γ] [inst_1 : EMetricSpace β] {f : γ → β},
UniformEmbedding f ↔
(∀ ε > 0, ∃ δ > 0, ∀ {a b : γ}, edist a b < δ → edist (f a) (f b) < ε) ∧
∀ δ > 0, ∃ ε > 0, ∀ {a b : γ}, edist (f a) (f b) < ε → edist a b < δ
The theorem states that for any function `f` mapping between two extended metric spaces (types `γ` and `β`), `f` is a uniform embedding if and only if two conditions are satisfied: First, for any positive number `ε`, there exists a positive number `δ`, such that if the extended distance (`edist`) between any two points `a` and `b` in `γ` is less than `δ`, then the extended distance between their images under `f` in `β` is less than `ε`. Second, for any positive number `δ`, there exists a positive number `ε`, such that if the extended distance between the images of any two points `a` and `b` under `f` is less than `ε`, then the extended distance between the original points in `γ` is less than `δ`. In informal terms, the theorem shows that `f` is a uniform embedding if and only if it preserves the distances between points in both directions (from `γ` to `β` and vice versa).
More concisely: A function between two extended metric spaces is a uniform embedding if and only if for every ε > 0, there exists δ > 0 such that edist(a, b) < δ implies edist(f(a), f(b)) < ε, and for every δ > 0, there exists ε > 0 such that edist(f(a), f(b)) < ε implies edist(a, b) < δ.
|
edist_le_range_sum_of_edist_le
theorem edist_le_range_sum_of_edist_le :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {f : ℕ → α} (n : ℕ) {d : ℕ → ENNReal},
(∀ {k : ℕ}, k < n → edist (f k) (f (k + 1)) ≤ d k) → edist (f 0) (f n) ≤ (Finset.range n).sum fun i => d i
The theorem `edist_le_range_sum_of_edist_le` states that for any type `α` equipped with a pseudo extended metric space and any function `f` from natural numbers to `α`, if for every natural number `k` less than a given natural number `n`, the extended distance (or `edist`) between `f k` and `f (k + 1)` is less than or equal to some function `d k`, then the extended distance between `f 0` and `f n` is less than or equal to the sum of the function `d` over the range of natural numbers less than `n`. This theorem is a version of `edist_le_range_sum_edist` but with each intermediate distance replaced with an upper estimate.
More concisely: For any pseudo extended metric space `α` and function `f : ℕ → α` such that `edist(f k, f (k + 1)) ≤ d k for all k < n, edist(f 0, f n) ≤ ∑\_{k < n} d k.
|
edist_triangle_right
theorem edist_triangle_right :
∀ {α : Type u} [inst : PseudoEMetricSpace α] (x y z : α), edist x y ≤ edist x z + edist y z
The `edist_triangle_right` theorem, which is given for any type `α` in a pseudo e-metric space, states that for any three elements `x`, `y`, and `z` of this type, the e-distance (denoted as `edist`) from `x` to `y` is always less than or equal to the sum of the e-distance from `x` to `z` and the e-distance from `y` to `z`. This theorem is essentially the triangle inequality for e-metric spaces in Lean 4.
More concisely: For any e-metric space type `α`, the e-distance `edist(x, y)` between elements `x` and `y` is less than or equal to `edist(x, z) + edist(z, y)` for all `x`, `y`, and `z` of type `α`.
|
EMetric.mem_ball
theorem EMetric.mem_ball :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {x y : α} {ε : ENNReal}, y ∈ EMetric.ball x ε ↔ edist y x < ε := by
sorry
This theorem states that for any pseudo extended metric space `α`, given any two points `x` and `y` in that space `α` and an extended nonnegative real number `ε`, the point `y` belongs to the `ε`-ball centered at `x` if and only if the extended distance from `y` to `x` is less than `ε`. It is essentially defining what it means for a point to be within a certain "distance" (in this case, an extended distance) from another point in a pseudo extended metric space: it is in the `ε`-ball around that point.
More concisely: In a pseudo extended metric space, a point belongs to the extended ε-ball around another point if and only if the extended distance between them is less than ε.
|
EMetric.isOpen_ball
theorem EMetric.isOpen_ball :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {ε : ENNReal}, IsOpen (EMetric.ball x ε)
This theorem states that for any type `α` that has a `PseudoEMetricSpace` structure, any point `x` of type `α`, and any extended nonnegative real number `ε`, the ε-ball around `x` in the pseudometric space is an open set. In mathematical terms, considering a pseudometric space, the ball of radius `ε` centered at a point `x` is always an open set. The ball of radius `ε` around `x` (denoted `EMetric.ball x ε` in Lean 4) is defined as the set of all points `y` such that the extended distance (edist) between `y` and `x` is less than `ε`.
More concisely: For any pseudometric space (α, d) and point x ∈ α, the ε-ball B(x, ε) = {y ∈ α | edist(x, y) < ε} is an open set in α.
|
Mathlib.Topology.EMetricSpace.Basic._auxLemma.14
theorem Mathlib.Topology.EMetricSpace.Basic._auxLemma.14 :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {x y : α} {ε : ENNReal},
(y ∈ EMetric.closedBall x ε) = (edist y x ≤ ε)
The theorem `Mathlib.Topology.EMetricSpace.Basic._auxLemma.14` states that for any pseudo-emetric space `α`, and any elements `x` and `y` of `α`, and for any extended nonnegative real number `ε`, `y` is in the closed ε-ball centered at `x` (denoted by `EMetric.closedBall x ε`) if and only if the extended distance (`edist`) from `y` to `x` is less than or equal to `ε`. In simple terms, it verifies that the definition of a closed ball in a pseudo-emetric space `α` correctly encapsulates all points `y` whose distance to a given point `x` is at most `ε`.
More concisely: For any pseudo-metric space `α`, and any `x`, `y` in `α` and `ε` in the extended nonnegative reals, `y` belongs to the closed ε-ball centered at `x` if and only if the extended distance from `x` to `y` is less than or equal to `ε`.
|
edist_eq_zero
theorem edist_eq_zero : ∀ {γ : Type w} [inst : EMetricSpace γ] {x y : γ}, edist x y = 0 ↔ x = y
This theorem establishes a characteristic of points in an extended metric space. Specifically, for any two points 'x' and 'y' in a given extended metric space 'γ', the theorem states that the extended distance between 'x' and 'y' is zero if and only if 'x' and 'y' are the same point. The extended distance between two points is a generalization of the concept of distance that allows for the possibility of infinite distances.
More concisely: In an extended metric space, two points have zero extended distance if and only if they are equal.
|
EMetric.subset_countable_closure_of_compact
theorem EMetric.subset_countable_closure_of_compact :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {s : Set α}, IsCompact s → ∃ t ⊆ s, t.Countable ∧ s ⊆ closure t := by
sorry
This theorem states that for any compact set in a pseudo emetric space, it is a separable set. In other words, this compact set can be written as a subset of the closure of a countable set. More explicitly, given a compact set within a pseudo emetric space, there exists a countable set which is contained within the original set, and the closure of this countable set contains the entire original set.
More concisely: Every compact subset of a pseudo metric space is separable.
|
EMetric.inseparable_iff
theorem EMetric.inseparable_iff :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {x y : α}, Inseparable x y ↔ edist x y = 0
The theorem `EMetric.inseparable_iff` states that for any pair of points `x` and `y` in a pseudo-emetric space `α`, the points are inseparable if and only if the extended distance between `x` and `y` is zero. This means, in the context of a pseudo-emetric space, two points are considered inseparable exactly when they have zero distance between them.
More concisely: In a pseudo-metric space, two points are inseparable if and only if their extended distance is zero.
|
EMetric.uniformContinuousOn_iff
theorem EMetric.uniformContinuousOn_iff :
∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β} {s : Set α},
UniformContinuousOn f s ↔
∀ ε > 0, ∃ δ > 0, ∀ {a : α}, a ∈ s → ∀ {b : α}, b ∈ s → edist a b < δ → edist (f a) (f b) < ε
This theorem provides an ε-δ characterization of uniform continuity on a set for pseudoemetric spaces. In more detail, it states that for any function `f` mapping from type `α` to `β`, and a set `s` of type `α`, where `α` and `β` are both pseudoemetric spaces, `f` is uniformly continuous on `s` if and only if for every ε greater than 0, there exists a δ greater than 0 such that for any two elements `a` and `b` in `s`, if the pseudoemetric distance between `a` and `b` is less than δ, then the pseudoemetric distance between `f(a)` and `f(b)` is less than ε. In simple terms, no matter where in the set `s` we are, if two points are sufficiently close together, their images under `f` will also be close together.
More concisely: A function between pseudometric spaces is uniformly continuous on a set if and only if for every ε > 0, there exists δ > 0 such that the pseudometric distances between any two points in the set with distance less than δ have images under the function with distance less than ε.
|
EMetric.mem_ball_self
theorem EMetric.mem_ball_self :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {ε : ENNReal}, 0 < ε → x ∈ EMetric.ball x ε
The theorem `EMetric.mem_ball_self` states that, for any pseudo extended metric space `α`, any point `x` in `α`, and any extended nonnegative real number `ε` greater than zero, `x` is an element of the ball of radius `ε` centered at `x`. In other words, it asserts that in any such metric space, each point belongs to the open ball centered at itself, provided the radius of that ball is greater than zero. This is a fundamental property of metric spaces, reflecting the idea that a ball can be thought of as including all points within a certain "distance" from its center.
More concisely: For any pseudo extended metric space and any point with positive distance from itself, that point belongs to the open ball of that radius centered at itself.
|
Mathlib.Topology.EMetricSpace.Basic._auxLemma.13
theorem Mathlib.Topology.EMetricSpace.Basic._auxLemma.13 :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {x y : α} {ε : ENNReal}, (y ∈ EMetric.ball x ε) = (edist y x < ε) := by
sorry
This theorem states that for any type `α` equipped with a pseudo extended metric space structure, and any two points `x` and `y` of type `α` and a nonnegative real number `ε`, the condition that `y` is in the ε-ball centered at `x` is equivalent to the extended distance between `y` and `x` being less than `ε`. In other words, a point `y` lies within the ε-ball around a point `x` if and only if the extended distance from `y` to `x` is less than `ε`.
More concisely: For any pseudo extended metric space `(α, d)`, given points `x, y : α` and a nonnegative real `ε`, the conditions `y ∈ ε-ball x` and `d(x, y) < ε` are equivalent.
|
EMetric.uniformEmbedding_iff
theorem EMetric.uniformEmbedding_iff :
∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β},
UniformEmbedding f ↔
Function.Injective f ∧
UniformContinuous f ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, edist (f a) (f b) < ε → edist a b < δ
This theorem provides the ε-δ characterization of uniform embeddings in pseudoemetric spaces. For any two types `α` and `β` that are pseudoemetric spaces, and a function `f` from `α` to `β`, the function `f` is a uniform embedding if and only if the following three conditions hold:
1. `f` is injective, meaning for any two elements in `α`, if their images under `f` are equal then the two elements must be the same.
2. `f` is uniformly continuous, which implies that for any point in `α`, if it is close to another point, then their images under `f` are also close to each other.
3. For any `δ` greater than 0, there exists `ε` greater than 0 such that for any pair of elements `(a, b)` in `α`, if the pseudoemetric distance (edist) between `f(a)` and `f(b)` is less than `ε`, then the pseudoemetric distance between `a` and `b` is less than `δ`.
This theorem is a key property of uniform embeddings in pseudoemetric spaces, allowing us to work with distances and continuity in a uniform way.
More concisely: A function between two pseudometric spaces is a uniform embedding if and only if it is injective, uniformly continuous, and satisfies the inverse triangle inequality for arbitrary δ > 0, there exists ε > 0 such that edist(fa, fb) < ε implies edist(a, b) < δ.
|
EMetric.countable_closure_of_compact
theorem EMetric.countable_closure_of_compact :
∀ {γ : Type w} [inst : EMetricSpace γ] {s : Set γ}, IsCompact s → ∃ t ⊆ s, t.Countable ∧ s = closure t
The theorem `EMetric.countable_closure_of_compact` states that for any compact set in an extended metric space, it is separable. In other words, this compact set is the closure of a countable set. Given any compact set `s` in an extended metric space `γ`, there exists a set `t` which is a subset of `s` and is countable, such that the closure of `t` is equal to `s`.
More concisely: A compact subset of an extended metric space is the closure of a countable set.
|
EMetric.cauchySeq_iff'
theorem EMetric.cauchySeq_iff' :
∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : Nonempty β] [inst_2 : SemilatticeSup β]
{u : β → α}, CauchySeq u ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, edist (u n) (u N) < ε
This theorem provides a variation around the emetric characterization of Cauchy sequences. Specifically, it states that for any types `α` and `β`, where `α` is a type with a pseudo-emetric space structure, `β` is a nonempty type with a semilattice sup structure, and `u` is a function from `β` to `α` (i.e., a sequence in `α` indexed by `β`), `u` is a Cauchy sequence if and only if for every real number `ε` greater than 0, there exists an element `N` in `β` such that for all `n` in `β` that are greater than or equal to `N`, the extended metric distance between `u(n)` and `u(N)` is less than `ε`. This captures the intuition that in a Cauchy sequence, the terms get arbitrarily close to each other as the sequence progresses.
More concisely: For any pseudo-metric space `(α, d)` and semilattice `(β, ⊔)`, a sequence `u : β → α` is Cauchy if and only if for every `ε > 0`, there exists `N ∈ β` such that `d(u(n), u(N)) < ε` for all `n ≥ N`.
|
Subtype.edist_eq
theorem Subtype.edist_eq :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {p : α → Prop} (x y : Subtype p), edist x y = edist ↑x ↑y
This theorem states that in a pseudoemetric space, the extended pseudodistance on a subset is the same as the original pseudodistance. Specifically, given any pseudoemetric space and a property that defines a subset of that space, for any two elements in the subset, their extended pseudodistance is equal to the pseudodistance of their corresponding elements in the original space.
More concisely: In a pseudometric space, the extended pseudodistance between any two points in a subset equals the pseudodistance between their corresponding points in the original space.
|
EMetric.tendstoUniformlyOn_iff
theorem EMetric.tendstoUniformlyOn_iff :
∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] {ι : Type u_2} {F : ι → β → α} {f : β → α} {p : Filter ι}
{s : Set β}, TendstoUniformlyOn F f p s ↔ ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, edist (f x) (F n x) < ε
The theorem `EMetric.tendstoUniformlyOn_iff` states that for any types `α`, `β`, and `ι` with `α` being a PseudoEMetricSpace, any sequence of functions `F` from `ι` to the function space from `β` to `α`, any function `f` from `β` to `α`, any filter `p` on `ι`, and any set `s` of `β`, the sequence `F` converges uniformly to `f` on the set `s` with respect to the filter `p` if and only if for all `ε` greater than 0, eventually for every `n` in `p` and every `x` in `s`, the extended distance between `f(x)` and `F(n, x)` is less than `ε`.
More concisely: A sequence of functions from a filter converges uniformly to a function on a set with respect to that filter if and only if for every ε > 0, eventually for all n in the filter and all x in the set, the extended distance between the functions' values at x is less than ε.
|
uniformity_pseudoedist
theorem uniformity_pseudoedist :
∀ {α : Type u} [inst : PseudoEMetricSpace α],
uniformity α = ⨅ ε, ⨅ (_ : ε > 0), Filter.principal {p | edist p.1 p.2 < ε}
This theorem, `uniformity_pseudoedist`, states that for any type `α` which is a pseudo-emetric space, the uniformity structure on `α` can be reformulated in terms of the 'extended distance'. Specifically, the uniformity is equal to the infimum over all positive `ε` of the principal filter of the set of all pairs `p` such that the extended distance between the first and second elements of `p` is less than `ε`. In mathematical terms, this is saying that the uniformity is the greatest lower bound of the collection of all principal filters of sets where the extended distance between elements is less than a positive real number.
More concisely: The uniformity of a pseudo-metric space `α` is equal to the infimum of the principal filters of sets where the extended distance between any two elements is less than a positive real number.
|
EMetric.diam_mono
theorem EMetric.diam_mono :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {s t : Set α}, s ⊆ t → EMetric.diam s ≤ EMetric.diam t
The theorem `EMetric.diam_mono` states that in any pseudoemetric space `α`, the diameter of a set is monotonic with respect to inclusion. More specifically, given any two sets `s` and `t` of type `α`, if `s` is a subset of `t` (denoted by `s ⊆ t`), then the diameter of `s` is less than or equal to the diameter of `t`. Here, the diameter of a set is defined as the supremum of the distances between all pairs of points in the set.
More concisely: In any pseudometric space, the diameter of a subset is less than or equal to the diameter of any larger set it is contained in.
|
EMetric.mk_uniformity_basis_le
theorem EMetric.mk_uniformity_basis_le :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {β : Type u_2} {p : β → Prop} {f : β → ENNReal},
(∀ (x : β), p x → 0 < f x) →
(∀ (ε : ENNReal), 0 < ε → ∃ x, p x ∧ f x ≤ ε) → (uniformity α).HasBasis p fun x => {p | edist p.1 p.2 ≤ f x}
This theorem states that, given a function `f : β → ℝ≥0∞` mapping from an arbitrary type `β` to the extended nonnegative real numbers, if `f` maps the set of elements `{i | p i}` to a set of positive numbers that accumulate to zero, then the closed `f i`-neighborhoods of the diagonal constitute a basis for the uniformity `𝓤 α` on a pseudo-emetric space `α`. Here, a `f i`-neighborhood of the diagonal is defined as the set of pairs `p` such that the extended distance `edist` between the elements of `p` is less than or equal to `f i`. The theorem requires two conditions - all elements `x` in `{i | p i}` must map to a positive value through `f`, and for any positive extended nonnegative real number `ε`, there must exist an `x` in `{i | p i}` such that `f x` is less than or equal to `ε`. If these two conditions hold, then the set of `f i`-neighborhoods of the diagonal form a basis for the uniform structure on the pseudo-emetric space.
More concisely: Given a function `f : β → ℝ≥0∞` and a pseudo-metric space `α`, if `f` maps the subset of `β` where `f(x) > 0` to positive numbers accumulating to zero, then the collection of `f i`-neighborhoods of the diagonal forms a basis for the uniformity on `α`.
|
EMetric.tendstoLocallyUniformlyOn_iff
theorem EMetric.tendstoLocallyUniformlyOn_iff :
∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] {ι : Type u_2} [inst_1 : TopologicalSpace β]
{F : ι → β → α} {f : β → α} {p : Filter ι} {s : Set β},
TendstoLocallyUniformlyOn F f p s ↔
∀ ε > 0, ∀ x ∈ s, ∃ t ∈ nhdsWithin x s, ∀ᶠ (n : ι) in p, ∀ y ∈ t, edist (f y) (F n y) < ε
The theorem `EMetric.tendstoLocallyUniformlyOn_iff` provides a condition for locally uniform convergence of a sequence of functions on a set. Specifically, it states that for every `α` and `β` which are types with `α` being a pseudo-emetric space and `β` being a topological space, a sequence of functions `F` from `ι` to `β` to `α`, a function `f` from `β` to `α`, a filter `p` on `ι` and a set `s` of `β`, `F` tends to `f` locally uniformly on `s` under `p` if and only if for every `ε` greater than 0, for every `x` in `s`, there exists a `t` in the neighborhood within `s` of `x` such that for all future `n` in `p`, for every `y` in `t`, the extended distance between `f(y)` and `F(n, y)` is less than `ε`. Essentially, this theorem is a definition of locally uniform convergence in terms of extended distances.
More concisely: A sequence of functions from a pseudo-metric space to another topological space converges locally uniformly to a function on a subset under a filter if and only if for every ε > 0 and x in the subset, there exists a neighborhood of x containing a point y such that the extended distance between the function values at y from the sequence and the limiting function is less than ε for all sufficiently large indices in the filter.
|
EMetric.diam_empty
theorem EMetric.diam_empty : ∀ {α : Type u} [inst : PseudoEMetricSpace α], EMetric.diam ∅ = 0
This theorem states that the diameter of an empty set in a pseudoemetric space always equals zero. In other words, if we have a set in some pseudoemetric space and that set is empty, then the supremum of the extended distances between any two points in the set (which is defined as the diameter) is zero.
More concisely: In a pseudometric space, the diameter of an empty set is 0.
|
edist_congr_right
theorem edist_congr_right :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {x y z : α}, edist x y = 0 → edist x z = edist y z
This theorem states that in any pseudoemetric space, if the extended distance between two points `x` and `y` is zero, then the extended distance between `x` and a third point `z` is the same as the extended distance between `y` and `z`. In other words, if `x` and `y` are at the exact same location in the space, then the distance from either of them to `z` is the same.
More concisely: In a pseudometric space, if the extended distance between two points is zero, then the extended distance between any one of them and a third point is equal.
|
mem_uniformity_edist
theorem mem_uniformity_edist :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {s : Set (α × α)},
s ∈ uniformity α ↔ ∃ ε > 0, ∀ {a b : α}, edist a b < ε → (a, b) ∈ s
This theorem characterizes the elements of the uniformity in a pseudo-emetric space in terms of the extended distance. For any type `α` that is a pseudo-emetric space, and any set `s` of pairs of elements of `α`, the theorem states that `s` is in the uniformity of `α` if and only if there exists a positive real number `ε` such that for all pairs `(a, b)` of elements of `α`, if the extended distance between `a` and `b` is less than `ε`, then the pair `(a, b)` is in `s`.
More concisely: A set `s` of pairs of elements in a pseudo-metric space `α` lies in the uniformity of `α` if and only if there exists a positive real number `ε` such that every pair of elements `a` and `b` with extended distance less than `ε` is in `s`.
|
EMetric.complete_of_convergent_controlled_sequences
theorem EMetric.complete_of_convergent_controlled_sequences :
∀ {α : Type u} [inst : PseudoEMetricSpace α] (B : ℕ → ENNReal),
(∀ (n : ℕ), 0 < B n) →
(∀ (u : ℕ → α),
(∀ (N n m : ℕ), N ≤ n → N ≤ m → edist (u n) (u m) < B N) → ∃ x, Filter.Tendsto u Filter.atTop (nhds x)) →
CompleteSpace α
This theorem states that a pseudometric space is complete if and only if all sequences, which satisfy a certain type of bound, are converging. Specifically, if we have a sequence in the space and a sequence of nonnegative real numbers, with each number in the latter sequence being greater than zero, such that the distance between any two terms in the sequence is less than or equal to the corresponding term in the nonnegative real numbers sequence (for any given index, all terms after this index in the sequence satisfy this property), then there exists a limit that the sequence converges to. This is often applied with a very fast convergence to `0` such as the sequence `B N = 2^{-N}`. The theorem allows us to use the technique of converging series, which is generally not possible for arbitrary Cauchy sequences.
More concisely: A pseudometric space is complete if and only if every Cauchy sequence in the space has a limit.
|