LeanAide documentation

LeanAide GPT-4 documentation

Module: Mathlib.Topology.MetricSpace.PseudoMetric

`Metric.isBounded_iff` theorem Metric.isBounded_iff : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α}, Bornology.IsBounded s ↔ ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C This theorem, `Metric.isBounded_iff`, asserts that for any type `α`, which is an instance of `PseudoMetricSpace`, and any set `s` of type `α`, the set `s` is bounded in the sense of the bornology i.e., `Bornology.IsBounded s` if and only if there exists a real number `C` such that for all elements `x` and `y` in the set `s`, the distance between `x` and `y` (i.e., `dist x y`) is less than or equal to `C`. This theorem is essentially characterizing the boundedness of a set in a metric (or pseudometric) space using the concept of bornology. More concisely: A set in a pseudometric space is bounded with respect to the bornology if and only if there exists a real number C such that the distance between any two elements in the set is less than or equal to C.
`Metric.mem_nhds_iff` theorem Metric.mem_nhds_iff : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {s : Set α}, s ∈ nhds x ↔ ∃ ε > 0, Metric.ball x ε ⊆ s := by sorry This theorem states that for a given type `α` equipped with a `PseudoMetricSpace` structure, a set `s` is a neighborhood of a point `x` (i.e., `s` belongs to the neighborhood filter of `x`) if and only if there exists a positive real number `ε` such that the metric ball centered at `x` with radius `ε` is a subset of `s`. In other words, a set is a neighborhood of a point in a pseudometric space if and only if it contains an open ball around that point. More concisely: A set is a neighborhood of a point in a pseudometric space if and only if it contains the open ball around that point.
`nhds_comap_dist` theorem nhds_comap_dist : ∀ {α : Type u} [inst : PseudoMetricSpace α] (a : α), Filter.comap (fun x => dist x a) (nhds 0) = nhds a This theorem, `nhds_comap_dist`, states that for any given pseudometric space `α` and any element `a` from this space, the neighborhood filter (`nhds`) at `a` is equal to the filter obtained by mapping every element `x` in the space to the distance from `x` to `a` (`dist x a`), and then taking the preimage of the neighborhood filter at `0` under this mapping. In other words, the "neighborhoods" of a point `a` in a pseudometric space are precisely the preimages of the "neighborhoods" of `0` under the distance function from `a`. More concisely: For any pseudometric space and element, the neighborhood filter at that element is equal to the preimage under the distance function of the neighborhood filter at 0.
`Metric.dist_mem_uniformity` theorem Metric.dist_mem_uniformity : ∀ {α : Type u} [inst : PseudoMetricSpace α] {ε : ℝ}, 0 < ε → {p \| dist p.1 p.2 < ε} ∈ uniformity α This theorem states that for any pseudometric space `α` and any positive real number `ε`, the set of all pairs `p` such that the distance between the elements of `p` is less than `ε` is an element of the `uniformity` of `α`. In other words, any neighborhood of the diagonal of a given constant size `ε` is considered an entourage (a neighborhood of the diagonal in the product space) in the uniformity (a specific type of filter) of the pseudometric space. More concisely: For any pseudometric space `α` and positive real number `ε`, the closed ball of radius `ε` around the diagonal is an entourage in the uniformity of `α`.
`coe_nndist` theorem coe_nndist : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x y : α), ↑(nndist x y) = dist x y This theorem states that for any pseudometric space `α`, the nonnegative real number distance (`nndist`) between any two points `x` and `y` in `α`, when coerced to a real number (`↑`), is equal to the regular distance (`dist`) between `x` and `y`. In other words, in any pseudometric space, the nonnegative distance and the conventional distance between any two points are essentially the same, the only difference being their respective types (nonnegative real numbers vs. real numbers). More concisely: For any pseudometric space, the coerced non-negative real distance between two points equals the regular distance between them. (i.e., ↑(nndist x y) = dist x y)
`Metric.isClosed_ball` theorem Metric.isClosed_ball : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε : ℝ}, IsClosed (Metric.closedBall x ε) The theorem `Metric.isClosed_ball` states that for any pseudometric space `α`, any point `x` in `α`, and any real number `ε`, the closed ball centered at `x` with radius `ε` (which is the set of all points `y` such that the distance between `y` and `x` is less than or equal to `ε`) is a closed set. In the context of topology, a set is called closed if it contains all its limit points. More concisely: In a pseudometric space, the closed ball is a closed set.
`dist_le_range_sum_of_dist_le` theorem dist_le_range_sum_of_dist_le : ∀ {α : Type u} [inst : PseudoMetricSpace α] {f : ℕ → α} (n : ℕ) {d : ℕ → ℝ}, (∀ {k : ℕ}, k < n → dist (f k) (f (k + 1)) ≤ d k) → dist (f 0) (f n) ≤ (Finset.range n).sum fun i => d i This theorem is in the context of a pseudo-metric space, which is a set where a notion of the distance between elements is given, satisfying certain conditions. Specifically, the theorem states that for any function `f` mapping natural numbers to elements of a pseudo-metric space, given an upper estimate function `d` for the distance between consecutive elements of the sequence generated by `f`, if for every natural number `k` less than `n` the distance between `f(k)` and `f(k + 1)` is less than or equal to `d(k)`, then the distance between `f(0)` and `f(n)` is less than or equal to the sum of `d(i)` for all `i` in the set of natural numbers less than `n`. In other words, the total distance travelled by the sequence `f` is bounded by the sum of these upper estimates `d(i)`. More concisely: Given a pseudo-metric space and a function mapping natural numbers to elements in it with an upper estimate of the distance between consecutive function values, if the distance between any two consecutive values is less than or equal to the estimate, then the total distance between the first and last values is less than or equal to the sum of the estimates for the distances between all preceding pairs.
`Dist.ext` theorem Dist.ext : ∀ {α : Type u_3} (x y : Dist α), dist = dist → x = y This theorem, `Dist.ext`, states that for all types `α` and any two distributions `x` and `y` of type `α`, if their distance functions are equal, then the two distributions `x` and `y` are also equal. Here, `dist` refers to a function that calculates the distance between two points. This theorem is fundamental in the context of probability distributions or any other mathematical constructs where a notion of distance is defined. More concisely: If for all types `α` and distributions `x` and `y` of type `α` in Lean 4, `dist x y` equals a constant `c`, then `x` equals `y`.
`dist_le_Ico_sum_dist` theorem dist_le_Ico_sum_dist : ∀ {α : Type u} [inst : PseudoMetricSpace α] (f : ℕ → α) {m n : ℕ}, m ≤ n → dist (f m) (f n) ≤ (Finset.Ico m n).sum fun i => dist (f i) (f (i + 1)) This theorem, named `dist_le_Ico_sum_dist`, establishes the triangle inequality for sequences of points with respect to the `Finset.Ico` definition. In the context of a given pseudometric space `α` and a function `f` mapping natural numbers to this space, if `m ≤ n`, then the distance between `f(m)` and `f(n)` is less than or equal to the sum of the distances between consecutive points in the `Finset.Ico` from `m` to `n`. This is a manifestation of the triangle inequality principle in the context of sequences of points in a pseudometric space. More concisely: For any pseudometric space α and function f mapping natural numbers to α, if m ≤ n then the distance between f(m) and f(n) is less than or equal to the sum of the distances between f(i+1) and f(i) for all i from m to n-1.
`Mathlib.Topology.MetricSpace.PseudoMetric._auxLemma.19` theorem Mathlib.Topology.MetricSpace.PseudoMetric._auxLemma.19 : ∀ {α : Type u} [inst : LT α] {x y : α}, (x > y) = (y < x) This theorem, from Mathlib about Topology and Metric Spaces, states that for any type `α` with an order relation `LT` (less than), and for any two elements `x` and `y` of that type, `x` is greater than `y` if and only if `y` is less than `x`. In other words, it confirms the relationship between "greater than" and "less than" operations in an ordered set. This type of reflexivity is fundamental to the definition of ordered sets, and is a commonly assumed axiom in fields such as mathematics and computer science. More concisely: For all types `α` with a total order `LT`, `x LT y` if and only if `yLTx`.
`finite_cover_balls_of_compact` theorem finite_cover_balls_of_compact : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α}, IsCompact s → ∀ {e : ℝ}, 0 < e → ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ x ∈ t, Metric.ball x e The theorem `finite_cover_balls_of_compact` states that for any compact set in a pseudometric space, there exists a finite collection of balls of a specified positive radius that fully covers the set. Specifically, given any type `α` that forms a pseudometric space, any compact set `s` of type `α`, and any positive real number `e`, there is a subset `t` of `s` which is finite, such that the set `s` is a subset of the union of balls with center `x` (where `x` is in `t`) and radius `e`. This theorem is a form of the finite cover property of compact sets in metric spaces. More concisely: For any compact subset `s` of a pseudometric space `α` and positive real number `e`, there exists a finite subset `t` of `s` such that `s` is covered by the balls centered at `t` with radius `e`.
`ball_pi` theorem ball_pi : ∀ {β : Type v} {π : β → Type u_3} [inst : Fintype β] [inst_1 : (b : β) → PseudoMetricSpace (π b)] (x : (b : β) → π b) {r : ℝ}, 0 < r → Metric.ball x r = Set.univ.pi fun b => Metric.ball (x b) r This theorem states that an open ball in a product space is a product of open balls. In mathematical terms, if we have a space that is a product of other spaces (each denoted by `π b` for each `b` in a finite type `β`), and a point `x` in this space, and a positive real number `r`, then the open ball centered at `x` with radius `r` in the product space is equal to the Cartesian product of the open balls centered at `x b` (the projection of `x` on each component space) with radius `r` in each component space. The theorem uses the notion of a pseudo metric space, which is a generalization of metric spaces where the distance between two different points can be zero. More concisely: In a pseudo metric space, the open ball centered at a point in the product of spaces is equal to the Cartesian product of open balls in each component space with the same radius.
`Mathlib.Topology.MetricSpace.PseudoMetric._auxLemma.7` theorem Mathlib.Topology.MetricSpace.PseudoMetric._auxLemma.7 : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x y : α} {ε : ℝ}, (y ∈ Metric.ball x ε) = (dist y x < ε) This theorem, `Mathlib.Topology.MetricSpace.PseudoMetric._auxLemma.7`, states that for any type `α` endowed with a pseudo-metric space structure, and for any elements `x` and `y` of this type, along with a real number `ε`, the proposition "the point `y` lies in the ε-ball centered at `x`" is equivalent to the proposition "the distance from `y` to `x` is less than `ε`". Here, `Metric.ball x ε` defines the ε-ball around `x`, meaning the set of all points that are less than `ε` distance away from `x`. More concisely: For any pseudo-metric space `(α, d)`, and for all `x, y : α` and `ε : ℝ`, the point `y` lies in the `ε`-ball `Metric.ball x ε` if and only if the distance `d(x y)` between `x` and `y` is less than `ε`.
`dist_le_range_sum_dist` theorem dist_le_range_sum_dist : ∀ {α : Type u} [inst : PseudoMetricSpace α] (f : ℕ → α) (n : ℕ), dist (f 0) (f n) ≤ (Finset.range n).sum fun i => dist (f i) (f (i + 1)) The theorem `dist_le_range_sum_dist` states that in any pseudometric space `α`, for any natural number `n` and any sequence of points `f` from natural numbers to `α`, the distance between the first point in the sequence (`f 0`) and the `n`-th point (`f n`) is less than or equal to the sum of the distances between each successive pair of points in the sequence from the first to the `n`-th. This is essentially a version of the triangle inequality for sequences of points, where `Finset.range n` represents a set of natural numbers less than `n`. More concisely: In any pseudometric space, the distance between the first and `n`-th points of a finite sequence of points satisfies the triangle inequality, that is, the sum of the distances between successive pairs of points from the first to the `n`-th point is an upper bound for the distance between the first and `n`-th points.
`Metric.mem_ball_self` theorem Metric.mem_ball_self : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε : ℝ}, 0 < ε → x ∈ Metric.ball x ε The theorem `Metric.mem_ball_self` states that for any type `α` that is a PseudoMetricSpace, any point `x` in `α`, and any real number `ε` greater than zero, `x` is an element of the metric ball centered at `x` with radius `ε`. In other words, in any pseudometric space, any point is within an open ball centered at itself with a positive radius. More concisely: For any pseudometric space (α, d), and any point x ∈ α and positive real number ε, x belongs to the metric ball B(x, ε) = {y ∈ α \| d(x, y) < ε}.
`Metric.ball_mem_nhds` theorem Metric.ball_mem_nhds : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x : α) {ε : ℝ}, 0 < ε → Metric.ball x ε ∈ nhds x The theorem `Metric.ball_mem_nhds` states that for any type `α`, endowed with a pseudometric space structure, and for any point `x` of type `α` and a positive real number `ε`, the metric ball centered at `x` with radius `ε` is a neighborhood of `x`. In mathematical terms, this means that the set of all points `y` such that the distance from `y` to `x` is less than `ε`, is a neighborhood of `x` according to the topology induced by the pseudometric space structure. More concisely: For any pseudometric space (α, d), and point x ∈ α, the metric ball B(x, ε) = {y ∈ α \| d(x, y) < ε} is a neighborhood of x.
`dist_triangle` theorem dist_triangle : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x y z : α), dist x z ≤ dist x y + dist y z := by sorry This theorem, known as the Triangle Inequality, applies to any pseudometric space. For any three points `x`, `y`, and `z` in this space, it asserts that the distance from `x` to `z` is less than or equal to the sum of the distances from `x` to `y` and from `y` to `z`. This is a fundamental property of distances in many mathematical spaces, including, for example, the Euclidean distance in real and complex spaces. More concisely: In any pseudometric space, the distance between any two points `x` and `y`, and the distance from `y` to a third point `z`, satisfies the inequality `d(x, z) ≤ d(x, y) + d(y, z)`.
`Metric.closure_ball_subset_closedBall` theorem Metric.closure_ball_subset_closedBall : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε : ℝ}, closure (Metric.ball x ε) ⊆ Metric.closedBall x ε := by sorry This theorem states that for any pseudometric space (a set equipped with a distance function satisfying certain properties), and any point 'x' of that space, the closure of the open ball around 'x' with radius 'ε' is a subset of the closed ball around 'x' with the same radius. Here, an open ball around 'x' with radius 'ε' is the set of all points whose distance to 'x' is less than 'ε', while a closed ball is the set of all points whose distance to 'x' is less than or equal to 'ε'. The closure of a set is the smallest closed set that contains it. In other words, any point that can be reached from the open ball by continually stepping to points arbitrarily close (but not equal to 'ε') is also within the closed ball. More concisely: For any pseudometric space and point, the closure of the open ball is contained in the closed ball with the same radius.
`Metric.emetric_closedBall_nnreal` theorem Metric.emetric_closedBall_nnreal : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε : NNReal}, EMetric.closedBall x ↑ε = Metric.closedBall x ↑ε This theorem states that for any pseudometric space `α`, any point `x` in that space, and any non-negative real number `ε`, the closed ball defined using the extended distance (`edist`) and the closed ball defined using the ordinary distance (`dist`) coincide. In other words, for every point in the pseudometric space, the set of all points within a certain non-negative real number distance, using either the extended distance or the ordinary distance, is the same. More concisely: For any pseudometric space, any point, and any non-negative real number, the closed balls defined using the extended distance and ordinary distance are equal.
`Metric.uniformity_basis_edist` theorem Metric.uniformity_basis_edist : ∀ {α : Type u} [inst : PseudoMetricSpace α], (uniformity α).HasBasis (fun ε => 0 < ε) fun ε => {p \| edist p.1 p.2 < ε} This theorem is expressing the uniformity in terms of `edist` in a PseudoMetricSpace. Specifically, for any type `α` that has a PseudoMetricSpace structure, the uniformity of `α` has a basis consisting of the sets of all pairs `(p.1, p.2)` such that the extended distance `edist` between `p.1` and `p.2` is less than some positive number `ε`. This means that the filter that defines the uniformity can be generated by considering these sets for all positive `ε`. More concisely: For any type `α` with a PseudoMetricSpace structure, the uniformity of `α` has a basis consisting of sets of pairs `(p.1, p.2)` with `edist(p.1, p.2) < ε` for some positive `ε`.
`Real.dist_eq` theorem Real.dist_eq : ∀ (x y : ℝ), dist x y = \|x - y\| This theorem states that for any two real numbers `x` and `y`, the distance between `x` and `y` is equal to the absolute value of their difference. In mathematical notation, for all x, y in ℝ, dist(x, y) = \|x - y\|. More concisely: For all real numbers x and y, the distance between x and y is equal to the absolute value of their difference: \|x - y\| = dist(x, y).
`Metric.mem_closure_iff` theorem Metric.mem_closure_iff : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} {a : α}, a ∈ closure s ↔ ∀ ε > 0, ∃ b ∈ s, dist a b < ε This theorem, termed as the "ε-characterization of the closure in pseudometric spaces", states that for any type `α` that is a PseudoMetric space, for any set `s` of elements of type `α`, and for any element `a` of type `α`, `a` is in the closure of `s` if and only if for all `ε` greater than 0, there exists an element `b` in `s` such that the distance between `a` and `b` is less than `ε`. In simpler terms, an element is in the closure of a set in a pseudometric space if for any small positive distance, there's a point in the set that is within that distance from the element. More concisely: In a pseudometric space, an element belongs to the closure of a set if and only if for every positive distance, there exists an element in the set within that distance.
`dist_comm` theorem dist_comm : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x y : α), dist x y = dist y x This theorem states that for any pseudo metric space, the distance function is commutative. In other words, for all elements `x` and `y` in some type `α` that forms a pseudo metric space, the distance from `x` to `y` is the same as the distance from `y` to `x`. This mirrors the real-world intuition that the distance between two points does not depend on the order in which we consider them. More concisely: For any pseudo metric space, the distance between two elements is symmetric.
`Metric.closedBall_zero'` theorem Metric.closedBall_zero' : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x : α), Metric.closedBall x 0 = closure {x} The theorem `Metric.closedBall_zero'` states that for any type `α` that is a pseudometric space, and for any element `x` of type `α`, the closed ball centered at `x` with radius 0 is equal to the closure of the singleton set `{x}`. In other words, the set of all points with a distance less than or equal to 0 from `x` is equivalent to the smallest closed set containing only `x`. More concisely: For any pseudometric space `α` and element `x` in `α`, the closed ball `{y : α \| d(x, y) ≤ 0}` is equal to the closure of the singleton set `{x}`.
`Metric.mk_uniformity_basis` theorem Metric.mk_uniformity_basis : ∀ {α : Type u} [inst : PseudoMetricSpace α] {β : Type u_3} {p : β → Prop} {f : β → ℝ}, (∀ (i : β), p i → 0 < f i) → (∀ ⦃ε : ℝ⦄, 0 < ε → ∃ i, p i ∧ f i ≤ ε) → (uniformity α).HasBasis p fun i => {p \| dist p.1 p.2 < f i} This theorem states that for any type `α` that is a pseudo metric space and any type `β`, given a function `f : β → ℝ` and a property `p : β → Prop`, if the function `f` maps the set `{i \| p i}` to a set of positive numbers that accumulates to zero, then the sets `{p \| dist p.1 p.2 < f i}`, where `i` satisfies property `p`, form a basis for the uniformity of `α`. In other words, any neighborhood of the diagonal in the uniformity of `α` can be made arbitrarily small by selecting appropriate `i` such that `p i` is true and `f i` is sufficiently small. This theorem provides a way to construct a basis for the uniformity in a pseudo metric space given a function that maps to a set of positive numbers that accumulate to zero. More concisely: Given a pseudo metric space `α`, a function `f : β → ℝ` mapping the set `{i : β \| p i}` to summable positive numbers, and a property `p : β → Prop`, the sets `{i : β \| p i}`, where `i` satisfies `dist p.1 p.2 < f i,` form a basis for the uniformity of `α`.
`nndist_triangle` theorem nndist_triangle : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x y z : α), nndist x z ≤ nndist x y + nndist y z This theorem is a statement of the triangle inequality for the nonnegative distance in any pseudo-metric space. Given any three points `x`, `y`, and `z` in such a space, the nonnegative distance from `x` to `z` is always less than or equal to the sum of the nonnegative distance from `x` to `y` and the nonnegative distance from `y` to `z`. This is a fundamental property of distances in these spaces. More concisely: In any pseudo-metric space, the non-negative distance from x to z is less than or equal to the sum of the non-negative distances from x to y and y to z.
`Metric.eventually_nhds_prod_iff` theorem Metric.eventually_nhds_prod_iff : ∀ {α : Type u} {ι : Type u_2} [inst : PseudoMetricSpace α] {f : Filter ι} {x₀ : α} {p : α × ι → Prop}, (∀ᶠ (x : α × ι) in nhds x₀ ×ˢ f, p x) ↔ ∃ ε > 0, ∃ pa, (∀ᶠ (i : ι) in f, pa i) ∧ ∀ {x : α}, dist x x₀ < ε → ∀ {i : ι}, pa i → p (x, i) This theorem, `Metric.eventually_nhds_prod_iff`, provides a specific condition for a property to hold eventually in the product of a neighborhood filter and another filter, within a pseudo-metric space. It says that a property `p` holds eventually for elements `(x, i)` in the product of the neighborhood filter at `x₀` and a filter `f`, if and only if there exists a positive real number `ε` and a predicate `pa` such that `pa i` holds eventually in filter `f`, and for all `x` and `i` such that the distance between `x` and `x₀` is less than `ε` and `pa i` holds, the property `p` holds for `(x, i)`. More concisely: A property holds eventually for elements in the product of a neighborhood filter at x\_0 and a filter if and only if there exists an ε and a predicate holding eventually in the filter such that the property holds for all elements within ε distance from x\_0 with the predicate satisfied.
`IsCompact.isSeparable` theorem IsCompact.isSeparable : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α}, IsCompact s → TopologicalSpace.IsSeparable s This theorem states that any compact set in a pseudo-metric space is separable. In detail, given a type `α` equipped with a pseudo-metric space structure, and a set `s` of this type, if `s` is compact (i.e., for every nontrivial filter `f` that contains `s`, there exists an element `a` in `s` such that every set of `f` meets every neighborhood of `a`), then `s` is also separable. That is, there exists a countable set `c` such that `s` is contained in the closure of `c`. More concisely: In a pseudo-metric space, every compact set is separable, meaning there exists a countable subset whose closure contains the compact set.
`Metric.sphere_subset_closedBall` theorem Metric.sphere_subset_closedBall : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε : ℝ}, Metric.sphere x ε ⊆ Metric.closedBall x ε This theorem states that for any pseudometric space of type `α`, every point `x` in `α`, and every real number `ε`, the sphere centered at `x` with radius `ε` is a subset of the closed ball centered at `x` with the same radius. The sphere consists of all points exactly `ε` distance from `x`, while the closed ball consists of all points at most `ε` distance from `x`, thus every point on the sphere is also in the closed ball. More concisely: For any pseudometric space and for all points `x` in the space and real number `ε`, the sphere with center `x` and radius `ε` is included in the closed ball with center `x` and radius `ε`.
`Mathlib.Topology.MetricSpace.PseudoMetric._auxLemma.47` theorem Mathlib.Topology.MetricSpace.PseudoMetric._auxLemma.47 : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x y : α}, (0 ≤ dist x y) = True This theorem states that in any pseudometric space `α`, the distance between any two points `x` and `y` in `α` is always non-negative. In more mathematical terms, for every `α` which is a PseudoMetricSpace, and for every `x` and `y` in `α`, `0 ≤ dist x y` will always be true. This is a basic property of distances in pseudometric spaces, reflecting the intuitive idea that distance cannot be a negative value. More concisely: In any pseudometric space, the distance between any two points is non-negative.
`Metric.closedBall_eq_empty` theorem Metric.closedBall_eq_empty : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε : ℝ}, Metric.closedBall x ε = ∅ ↔ ε < 0 The theorem `Metric.closedBall_eq_empty` states that for any pseudometric space `α` and for any point `x` in `α` and real number `ε`, the closed ball centered at `x` with radius `ε` is empty if and only if `ε` is less than zero. In mathematical terms, it's saying that in a pseudometric space, a closed ball of negative radius doesn't contain any points. More concisely: In a pseudometric space, the closed ball centered at a point with a negative radius is empty.
`Metric.tendsto_nhds` theorem Metric.tendsto_nhds : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] {f : Filter β} {u : β → α} {a : α}, Filter.Tendsto u f (nhds a) ↔ ∀ ε > 0, ∀ᶠ (x : β) in f, dist (u x) a < ε The theorem `Metric.tendsto_nhds` states that for any pseudometric space `α`, any filter `f` of type `β`, any function `u` from `β` to `α`, and any point `a` in `α`, the function `u` tends to the neighborhood filter of `a` (i.e. `u` approaches `a`) if and only if for all `ε > 0`, eventually (for all `x` in `f` beyond a certain point), the distance between `u(x)` and `a` is less than `ε`. In other words, `u(x)` gets arbitrarily close to `a` as `x` ranges over the elements of the filter `f`. More concisely: For any pseudometric space, filter, function, and point, a function tends to the neighborhood filter of a point if and only if the function values get arbitrarily close to that point for all filter elements beyond some point.
`nndist_pi_def` theorem nndist_pi_def : ∀ {β : Type v} {π : β → Type u_3} [inst : Fintype β] [inst_1 : (b : β) → PseudoMetricSpace (π b)] (f g : (b : β) → π b), nndist f g = Finset.univ.sup fun b => nndist (f b) (g b) The theorem `nndist_pi_def` states that for any finite type `β` and any type function `π` from `β` to some other type, given that every `b` of type `β` maps to a pseudo metric space via `π`, the non-negative distance (`nndist`) between two functions `f` and `g` (both of type `(b : β) → π b`) is equal to the supremum (greatest element) of the set of non-negative distances between `f b` and `g b` for all `b` in the universal finite set of type `β`. In other words, the non-negative distance between two functions on a finite set is determined by the greatest distance between their values. More concisely: For any finite type `β` and type functions `π : β → X` to a pseudo metric space `X`, the non-negative distance between two functions `f` and `g` (of type `β → π (β)`) is equal to the supremum of the non-negative distances between `f (b)` and `g (b)` for all `b` in `β`.
`Metric.ball_subset_closedBall` theorem Metric.ball_subset_closedBall : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε : ℝ}, Metric.ball x ε ⊆ Metric.closedBall x ε This theorem states that for any pseudometric space (a generalization of the metric space concept that allows for points at zero distance from each other), and any point and real number in this space, the open ball centered at this point with radius equal to this real number is a subset of the closed ball centered at the same point with the same radius. In simpler terms, the set of all points with a distance less than a certain value from a given point is always contained within the set of all points with a distance less than or equal to that same value from the given point. More concisely: For any pseudometric space and point, the open ball is a subset of the closed ball with the same center and radius.
`dist_nonneg` theorem dist_nonneg : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x y : α}, 0 ≤ dist x y This theorem states that for any two points `x` and `y` in any pseudo metric space `α`, the distance between `x` and `y` is always non-negative. In other words, you can't have a negative distance between two points in a pseudo metric space. This is a fundamental property of distances in these mathematical structures. More concisely: In any pseudo metric space, the distance between any two points is non-negative.
`Metric.totallyBounded_of_finite_discretization` theorem Metric.totallyBounded_of_finite_discretization : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α}, (∀ ε > 0, ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε) → TotallyBounded s The theorem `Metric.totallyBounded_of_finite_discretization` states that for any pseudometric space (a set with a distance function that satisfies all the properties of a metric except the requirement that points must be distinct if their distance is non-zero), if for any positive real number ε, there exists finite data from which any element of the space can be reproduced such that if the finite data for two elements of the space are equal, then the distance between these two elements is less than ε, then the set is totally bounded. In simpler terms, this theorem states that a pseudometric space is totally bounded if one can approximate any point in the space up to a desired precision using only a finite amount of data. More concisely: A pseudometric space is totally bounded if for every ε > 0, there exists a finite subset that approximates every point to within distance ε.
`PseudoMetricSpace.ext` theorem PseudoMetricSpace.ext : ∀ {α : Type u_3} {m m' : PseudoMetricSpace α}, PseudoMetricSpace.toDist = PseudoMetricSpace.toDist → m = m' := by sorry This theorem states that for any type `α`, if we have two pseudo metric space structures `m` and `m'` defined on it, and the distance function (`toDist`) of both these structures are the same, then the two structures `m` and `m'` are indeed the same. In other words, two pseudo metric space structures defined on the same type are completely determined by their distance functions. If the distance functions are equal, then the pseudo metric space structures are also equal. More concisely: If two pseudo metric spaces defined on the same type have equal distance functions, then they are equal as pseudo metric spaces.
`dist_triangle_left` theorem dist_triangle_left : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x y z : α), dist x y ≤ dist z x + dist z y This theorem, named 'dist_triangle_left', is a statement about pseudo metric spaces. It asserts that for any type 'α' which forms a pseudo metric space, and for any three elements 'x', 'y', and 'z' of this type, the distance from 'x' to 'y' is always less than or equal to the sum of the distances from 'z' to 'x' and 'z' to 'y'. This is a generalization of the triangle inequality to pseudo metric spaces. More concisely: In any pseudo metric space, the distance from x to y is less than or equal to the sum of the distances from z to x and z to y (triangle inequality).
`Metric.emetric_ball` theorem Metric.emetric_ball : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε : ℝ}, EMetric.ball x (ENNReal.ofReal ε) = Metric.ball x ε This theorem states that for any pseudometric space `α`, any point `x` in `α`, and any real number `ε`, the ball defined in terms of the extended metric around `x` with radius `ε` is the same as the ball defined in terms of the ordinary metric around `x` with radius `ε`. In other words, it says that the sets of points that are less than `ε` away from `x` according to the extended metric and the ordinary metric are the same. More concisely: For any pseudometric space `α`, any point `x` in `α`, and real number `ε`, the extended metric and ordinary metric balls centered at `x` with radius `ε` are equal.
`Metric.tendsto_nhds_nhds` theorem Metric.tendsto_nhds_nhds : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {f : α → β} {a : α} {b : β}, Filter.Tendsto f (nhds a) (nhds b) ↔ ∀ ε > 0, ∃ δ > 0, ∀ {x : α}, dist x a < δ → dist (f x) b < ε The theorem `Metric.tendsto_nhds_nhds` states that for any two types `α` and `β`, with each type having a pseudo metric space structure, and a function `f : α → β`, the function `f` tends to `b` at `a` (represented as `Filter.Tendsto f (nhds a) (nhds b)`) if and only if for every positive real number `ε`, there exists a positive real number `δ` such that for all `x` in `α`, if the distance between `x` and `a` is less than `δ`, then the distance between `f(x)` and `b` is less than `ε`. In simpler terms, this theorem is a formalization of the epsilon-delta definition of a limit in the context of metric spaces. It says that a function `f` approaches a limit `b` as its argument approaches `a` if we can make the function value `f(x)` arbitrarily close to `b` (closer than any given positive number `ε`), by choosing `x` sufficiently close to `a` (closer than some `δ` which depends on `ε`). More concisely: A function between two pseudo metric spaces tends to a limit at a point if and only if for every ε > 0, there exists δ > 0 such that the distance between any point in the domain closer than δ to the point and the image of that point under the function is less than ε.
`Metric.uniformity_basis_dist_le` theorem Metric.uniformity_basis_dist_le : ∀ {α : Type u} [inst : PseudoMetricSpace α], (uniformity α).HasBasis (fun x => 0 < x) fun ε => {p \| dist p.1 p.2 ≤ ε} This theorem states that for any type α that has a structure of a pseudo metric space, the uniformity filter on α has a basis formed by the sets of pairs whose distance is less than or equal to a given positive real number. In other words, the sets of pairs (a, b) from α such that the distance between a and b is less than or equal to a certain positive ε form a basis for the uniformity of α. This basis consists of "constant size closed neighborhoods of the diagonal", which means sets of points in α that are close to each other according to the metric of the pseudo metric space. More concisely: For any pseudo metric space (α, d), the sets {{(a, b) \| d(a, b) ≤ ε}} for ε > 0 form a basis for the uniformity on α.
`Metric.tendstoLocallyUniformly_iff` theorem Metric.tendstoLocallyUniformly_iff : ∀ {α : Type u} {β : Type v} {ι : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : TopologicalSpace β] {F : ι → β → α} {f : β → α} {p : Filter ι}, TendstoLocallyUniformly F f p ↔ ∀ ε > 0, ∀ (x : β), ∃ t ∈ nhds x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, dist (f y) (F n y) < ε The theorem `Metric.tendstoLocallyUniformly_iff` expresses the concept of locally uniform convergence in terms of the metric `dist`. According to this theorem, for any types `α`, `β`, and `ι` with `α` being a pseudometric space and `β` being a topological space, a sequence of functions `F` from `ι` to `β`→`α` converges locally uniformly to a limiting function `f` from `β` to `α` with respect to a filter `p` if and only if for any positive `ε` and any `x` in `β`, there exists a neighborhood `t` of `x` such that for all `n` in the filter `p` and all `y` in the neighborhood `t`, the distance between `f(y)` and `F(n,y)` is less than `ε`. More concisely: A sequence of functions from a filter to a metric space converges locally uniformly to a limiting function with respect to the filter if and only if for every ε > 0 and every x in the space, there exists a neighborhood of x such that for all n in the filter and all y in the neighborhood, the distance between the limiting function's value at y and the sequence's value at (n, y) is less than ε.
`Metric.ball_subset_ball` theorem Metric.ball_subset_ball : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε₁ ε₂ : ℝ}, ε₁ ≤ ε₂ → Metric.ball x ε₁ ⊆ Metric.ball x ε₂ := by sorry The theorem `Metric.ball_subset_ball` states that for any pseudometric space `α`, any point `x` in `α`, and any two real numbers `ε₁` and `ε₂`, if `ε₁` is less than or equal to `ε₂`, then the metric ball centered at `x` with radius `ε₁` is a subset of the metric ball centered at `x` with radius `ε₂`. In other words, all points that are less than `ε₁` distance away from `x` are also less than `ε₂` distance away from `x` when `ε₁ ≤ ε₂`. More concisely: For any pseudometric space and any point in it, the metric ball with a smaller radius is contained in the metric ball with a larger radius.
`totallyBounded_Icc` theorem totallyBounded_Icc : ∀ {α : Type u} [inst : PseudoMetricSpace α] [inst_1 : Preorder α] [inst_2 : CompactIccSpace α] (a b : α), TotallyBounded (Set.Icc a b) The theorem `totallyBounded_Icc` states that, for any type `α` which is a pseudometric space, has a preorder (an order relation that is reflexive and transitive), and has a compact interval [a, b], the closed interval [a, b] is totally bounded. In mathematical terms, this means that for any given metric `d` in the uniformity of `α`, there exists a finite set of points `t` such that every element in the interval [a, b] is `d`-near to at least one element in `t`. This property is fundamental in the study of compactness in metric spaces. More concisely: Given a pseudometric space `α` with a preorder and a compact interval `[a, b]`, the closed interval `[a, b]` is totally bounded, meaning for any metric `d` in the uniformity of `α`, there exists a finite set `t` such that every element in `[a, b]` is `d`-close to some element in `t`.
`uniformContinuous_dist` theorem uniformContinuous_dist : ∀ {α : Type u} [inst : PseudoMetricSpace α], UniformContinuous fun p => dist p.1 p.2 The theorem `uniformContinuous_dist` states that for any pseudo-metric space `α`, the distance function, which takes a pair of points in `α` and returns the distance between them, is uniformly continuous. In other words, given any two points `(x, y)` in `α`, as `(x, y)` gets arbitrarily close to some other pair `(a, b)`, the distances `dist(x, y)` and `dist(a, b)` also get arbitrarily close. This holds true regardless of the particular location of `(x, y)` and `(a, b)` in the metric space `α`. More concisely: The distance function in a pseudo-metric space is uniformly continuous.
`Metric.closedBall_eq_sphere_of_nonpos` theorem Metric.closedBall_eq_sphere_of_nonpos : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε : ℝ}, ε ≤ 0 → Metric.closedBall x ε = Metric.sphere x ε := by sorry This theorem states that in any pseudo metric space, for any point 'x' and any real number 'ε' that is less than or equal to zero, the closed ball centered at 'x' with radius 'ε' is equal to the sphere centered at 'x' with radius 'ε'. In other words, if the radius is non-positive, the set of all points with distance from 'x' less than or equal to 'ε' (closed ball) coincides with the set of all points with distance exactly 'ε' from 'x' (sphere). More concisely: In any pseudo-metric space, the closed ball and sphere with center 'x' and non-positive radius 'ε' are equal.
`dist_pi_le_iff` theorem dist_pi_le_iff : ∀ {β : Type v} {π : β → Type u_3} [inst : Fintype β] [inst_1 : (b : β) → PseudoMetricSpace (π b)] {f g : (b : β) → π b} {r : ℝ}, 0 ≤ r → (dist f g ≤ r ↔ ∀ (b : β), dist (f b) (g b) ≤ r) This theorem establishes a condition under which the distance between two functions `f` and `g` (mapping from type `β` to a pseudo-metric space `π b`) is less than or equal to a real number `r`. Specifically, given non-negative `r`, the theorem states that the distance between `f` and `g` is less than or equal to `r` if and only if the distance between `f(b)` and `g(b)` is less than or equal to `r` for every `b` in the finite type `β`. These distances are calculated in the pseudo-metric space `π b`. More concisely: The theorem states that the distance between functions `f` and `g` from type `β` to pseudo-metric space `π b`, with non-negative real number `r`, holds if and only if the distance between `f(b)` and `g(b)` in `π b` is less than or equal to `r` for all `b` in `β`.
`Metric.forall_of_forall_mem_ball` theorem Metric.forall_of_forall_mem_ball : ∀ {α : Type u} [inst : PseudoMetricSpace α] (p : α → Prop) (x : α), (∃ᶠ (R : ℝ) in Filter.atTop, ∀ y ∈ Metric.ball x R, p y) → ∀ (y : α), p y This theorem states that for any property `p` and any point `x` in a pseudo-metric space, if the property `p` holds for all points `y` contained within balls of an arbitrary large radius `R` centered at `x`, then the property `p` holds for all points `y` in the entire pseudo-metric space. In other words, if we can find an arbitrary large radius `R` such that for any point `y` within the distance `R` from `x`, `p` is true, then `p` is valid for all points `y`. This theorem is a kind of "local to global" principle in the context of a pseudo-metric space. More concisely: In a pseudo-metric space, if a property holds for all points within an arbitrarily large ball centered at a point, then the property holds for all points in the space.
`Metric.secondCountable_of_almost_dense_set` theorem Metric.secondCountable_of_almost_dense_set : ∀ {α : Type u} [inst : PseudoMetricSpace α], (∀ ε > 0, ∃ s, s.Countable ∧ ∀ (x : α), ∃ y ∈ s, dist x y ≤ ε) → SecondCountableTopology α This theorem states that a pseudometric space is second countable if, for any given positive real number `ε`, there exists a countable set that is `ε`-dense. In the context of pseudometric spaces, a set is `ε`-dense if, for any element in the space, there is an element in the set such that the distance between the two elements is less than or equal to `ε`. The theorem takes a proof of the existence of such a countable `ε`-dense set for any `ε > 0` and concludes that the pseudometric space has a second countable topology. More concisely: A pseudometric space is second countable if for every positive real `ε`, there exists a countable `ε`-dense set.
`Metric.mem_closedBall` theorem Metric.mem_closedBall : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x y : α} {ε : ℝ}, y ∈ Metric.closedBall x ε ↔ dist y x ≤ ε This theorem states that for any pseudo-metric space, a point `y` is in the closed ball centered at `x` with radius `ε` if and only if the distance from `y` to `x` is less than or equal to `ε`. In other words, it characterizes the membership of a point in a closed ball in terms of the distance between points in the metric space. More concisely: A point `y` lies in the closed ball with center `x` and radius `ε` in a pseudo-metric space if and only if the distance from `x` to `y` is less than or equal to `ε`.
`Metric.isOpen_iff` theorem Metric.isOpen_iff : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α}, IsOpen s ↔ ∀ x ∈ s, ∃ ε > 0, Metric.ball x ε ⊆ s := by sorry The theorem `Metric.isOpen_iff` is a characterization of open sets in a pseudometric space. It states that for any type `α` with a pseudometric space structure and for any set `s` of type `α`, the set `s` is open if and only if for every element `x` in `s`, there exists a number `ε` greater than zero such that the open ball centered at `x` with radius `ε` is a subset of `s`. In other words, every point in an open set is the center of some open ball completely contained in the set. More concisely: A subset of a pseudometric space is open if and only if each of its points is the center of some open ball entirely contained within the subset.
`Metric.eball_top_eq_univ` theorem Metric.eball_top_eq_univ : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x : α), EMetric.ball x ⊤ = Set.univ This theorem states that in a pseudometric space, an open ball with an infinite radius is equivalent to the whole space. More specifically, for any point `x` in a pseudometric space of type `α`, the set of all points `y` whose extended distance (`edist`) from `x` is less than infinity (`⊤`) is the same as the universal set (`Set.univ`). This implies that an open ball of infinite radius essentially includes all points in the pseudometric space. More concisely: In a pseudometric space, the open ball with infinite radius equals the universal set.
`IsCompact.finite_cover_balls` theorem IsCompact.finite_cover_balls : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α}, IsCompact s → ∀ {e : ℝ}, 0 < e → ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ x ∈ t, Metric.ball x e In natural language, this theorem states that for any compact set in a pseudometric space, there exists a finite collection of balls of a given positive radius that cover the set. More specifically, given a set `s` which is compact in a pseudometric space `α`, and a positive real number `e`, the theorem ensures the existence of a subset `t` of `s` that is finite, and such that `s` is a subset of the union of balls of radius `e` centered at points in `t`. In other words, every point in `s` is within a distance `e` of some point in `t`. In mathematical notation, this can be represented as: for every compact `s` and every `e > 0`, there exists `t ⊆ s` such that `t` is finite and `s ⊆ ⋃_{x ∈ t} B(x, e)`, where `B(x, e)` is the ball of radius `e` centered at `x`. More concisely: Given any compact set `s` in a pseudometric space and a positive real number `e`, there exists a finite subset `t` of `s` such that every point in `s` lies within distance `e` of some point in `t` (i.e., `s` is covered by the union of balls of radius `e` centered at points in `t`).
`edist_dist` theorem edist_dist : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x y : α), edist x y = ENNReal.ofReal (dist x y) := by sorry In a pseudometric space `α`, the theorem `edist_dist` states that for any two points `x` and `y` in `α`, the extended distance (or edistance) between `x` and `y` equals the application of the function `ENNReal.ofReal` to the ordinary distance between `x` and `y`. In plain words, the extended distance is the same as the ordinary distance, but converted to a non-negative extended real number with the help of `ENNReal.ofReal`. This function returns the original real number if it is non-negative, or zero otherwise. More concisely: In a pseudometric space, the extended distance between any two points equals the non-negative real number obtained by applying `ENNReal.ofReal` to the ordinary distance between them.
`continuous_dist` theorem continuous_dist : ∀ {α : Type u} [inst : PseudoMetricSpace α], Continuous fun p => dist p.1 p.2 This theorem states that for any type `α` equipped with a `PseudoMetricSpace` structure (a type of mathematical space where distances can be measured), the distance function that takes a pair of points and returns the distance between them is a continuous function. In mathematical terms, it states that for any points in this specific type of space, small changes in the input points result in small changes in the output value (distance). More concisely: The distance function of a `PseudoMetricSpace` is continuous.
`Metric.mem_sphere` theorem Metric.mem_sphere : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x y : α} {ε : ℝ}, y ∈ Metric.sphere x ε ↔ dist y x = ε This theorem states that for any type `α` that has a pseudometric space structure, any two elements `x` and `y` of `α`, and any real number `ε`, `y` belongs to the sphere with center `x` and radius `ε` if and only if the distance between `y` and `x` equals `ε`. In other words, it establishes the condition for an element `y` to be a part of the sphere defined around `x` with radius `ε` in the context of a pseudometric space. More concisely: In a pseudometric space, an element belongs to the sphere around another element with a given radius if and only if the distance between them equals the radius.
`Metric.uniformContinuous_iff` theorem Metric.uniformContinuous_iff : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {f : α → β}, UniformContinuous f ↔ ∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, dist a b < δ → dist (f a) (f b) < ε The theorem `Metric.uniformContinuous_iff` provides a criterion for checking the uniform continuity of a function between two pseudometric spaces. Specifically, it states that for all types `α` and `β` that are pseudometric spaces, a function `f : α → β` is uniformly continuous if and only if for every positive real number `ε`, there exists a positive real number `δ` such that for all 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 `ε`. In simpler terms, no matter where we are in `α`, if two points are sufficiently close together (within `δ`), their images under `f` are also close together (within `ε`). More concisely: A function between two pseudometric spaces is uniformly continuous if and only if for every ε > 0, there exists δ > 0 such that d(a, b) < δ implies d(f(a), f(b)) < ε, where d denotes the respective pseudometric.
`Metric.nhds_basis_ball` theorem Metric.nhds_basis_ball : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α}, (nhds x).HasBasis (fun x => 0 < x) (Metric.ball x) This theorem states that for any type `α` equipped with a pseudometric space structure, and any element `x` of `α`, the neighborhood filter at `x` has a basis given by the set of metric balls centered at `x` with a radius greater than zero. In other words, every neighborhood of `x` can be expressed as a union of such metric balls. In mathematical terms, the idea is that for each point in the pseudometric space, we can generate all its neighborhoods using "open balls" centered at the point with positive radii. More concisely: For any pseudometric space `(α, d)` and element `x` in `α`, the neighborhood filter of `x` is equal to the filter generated by the open metric balls centered at `x` with positive radii.
`Metric.closedBall_subset_closedBall` theorem Metric.closedBall_subset_closedBall : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε₁ ε₂ : ℝ}, ε₁ ≤ ε₂ → Metric.closedBall x ε₁ ⊆ Metric.closedBall x ε₂ This theorem states that for any type `α` that is a pseudometric space, and for any point `x` of type `α`, if `ε₁` is less than or equal to `ε₂` (both are real numbers), then the closed ball centered at `x` with radius `ε₁` is a subset of the closed ball centered at `x` with radius `ε₂`. In other words, if one ball has a smaller or equal radius compared to another, all points in the smaller (or equally-sized) ball are also contained in the larger ball. More concisely: For any pseudometric space `α` and point `x` in `α`, the closed ball `{y : α \| d(x, y) ≤ ε₁}` around `x` with radius `ε₁` is a subset of the closed ball `{y : α \| d(x, y) ≤ ε₂}` around `x` with radius `ε₂`, when `ε₁` is less than or equal to `ε₂`.
`dist_triangle_right` theorem dist_triangle_right : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x y z : α), dist x y ≤ dist x z + dist y z This theorem is a statement of the triangle inequality in the context of pseudometric spaces. Given any pseudometric space `α` and any three points `x`, `y`, `z` within that space, the distance between `x` and `y` is always less than or equal to the sum of the distance between `x` and `z`, and the distance between `y` and `z`. This is a fundamental property of distance in many geometric and algebraic structures. More concisely: In a pseudometric space, the distance between any two points is less than or equal to the sum of the distances between each point and a third point.
`dist_pi_lt_iff` theorem dist_pi_lt_iff : ∀ {β : Type v} {π : β → Type u_3} [inst : Fintype β] [inst_1 : (b : β) → PseudoMetricSpace (π b)] {f g : (b : β) → π b} {r : ℝ}, 0 < r → (dist f g < r ↔ ∀ (b : β), dist (f b) (g b) < r) This theorem, `dist_pi_lt_iff`, is stating a property about the distance between two functions `f` and `g` in a pseudo metric space over a finite type `β`. Specifically, for any positive real number `r`, the distance between these two functions `f` and `g` is less than `r` if and only if the distance between the values of `f` and `g` at any element of `β` is less than `r`. Here, `f` and `g` are functions mapping each element of `β` to the metric space `π b`. More concisely: For any functions `f` and `g` mapping a finite type `β` to a metric space `π b` and for any positive real number `r`, `∀ x ∈ β, d(f x, g x) < r` if and only if `d(f, g) < r`, where `d(f, g)` denotes the distance between `f` and `g`.
`sphere_pi` theorem sphere_pi : ∀ {β : Type v} {π : β → Type u_3} [inst : Fintype β] [inst_1 : (b : β) → PseudoMetricSpace (π b)] (x : (b : β) → π b) {r : ℝ}, 0 < r ∨ Nonempty β → Metric.sphere x r = (⋃ i, Function.eval i ⁻¹' Metric.sphere (x i) r) ∩ Metric.closedBall x r The theorem `sphere_pi` states that, for any type `β`, a function `π` from `β` to some type, a finite type instance for `β`, a pseudo metric space instance for each `π b` where `b` is an element of `β`, and a function `x` from `β` to `π b`, and any real number `r` that is either greater than zero or such that `β` is nonempty, the sphere of radius `r` centered at `x` in the product space is equal to the intersection of the union over all `i` in `β` of the preimage under the evaluation at `i` of the sphere of radius `r` centered at `x i` in the space `π i`, with the closed ball of radius `r` centered at `x` in the product space. In simpler terms, this theorem is stating a geometric property about spheres and closed balls in a product of metric spaces. More concisely: For any metric space `(β, π)` and `r > 0`, the sphere of radius `r` centered at `x` in the product space `∏i∈β πi` is equal to the intersection of the closed ball of radius `r` centered at `x` and the union of the spheres of radius `r` centered at `xi` in each `πi`.
`Metric.controlled_of_uniformEmbedding` theorem Metric.controlled_of_uniformEmbedding : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {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 < δ This theorem states that if there is a function `f` that uniformly embeds one pseudometric space into another, then the distance between the images `f(x)` and `f(y)` of any two points `x` and `y` in the original space can be controlled by manipulating the distance between `x` and `y` and vice versa. More specifically, for any positive distance `ε`, there exists some positive distance `δ` such that if the original points `x` and `y` are less than `δ` apart, their images `f(x)` and `f(y)` are less than `ε` apart. Similarly, for any positive distance `δ`, there exists some positive distance `ε` such that if the images `f(x)` and `f(y)` are less than `ε` apart, the original points `x` and `y` are less than `δ` apart. This theorem is a fundamental property of uniform embeddings in pseudometric spaces. More concisely: Given a uniform embedding `f` of a pseudometric space into another, there exist positive constants `ε` and `δ` such that `d(x, y) < δ` implies `d(f(x), f(y)) < ε` and `d(f(x), f(y)) < ε` implies `d(x, y) < δ`, where `d` denotes the original and image space distances.
`dist_pi_const` theorem dist_pi_const : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : Fintype β] [inst_2 : Nonempty β] (a b : α), (dist (fun x => a) fun x => b) = dist a b This theorem states that for any types `α` and `β`, where `α` is a pseudometric space and `β` is a finite, non-empty type, the distance between the constant functions that always return `a` and `b` (for any `a` and `b` in `α`) is the same as the distance between `a` and `b` themselves. In other words, in this specific context, the distance between two constant functions is simply the distance between their constant outputs. More concisely: For any pseudometric space `α` and finite, non-empty type `β`, the distance between constant functions `λ (x : α), a` and `λ (x : α), b` is equal to the distance `d` between `a` and `b` in `α`, i.e., `distance (λ (x : α), a) (λ (x : α), b) = d (a b)`.
`closedBall_pi'` theorem closedBall_pi' : ∀ {β : Type v} {π : β → Type u_3} [inst : Fintype β] [inst_1 : (b : β) → PseudoMetricSpace (π b)] [inst_2 : Nonempty β] (x : (b : β) → π b) (r : ℝ), Metric.closedBall x r = Set.univ.pi fun b => Metric.closedBall (x b) r This theorem states that in the context of a product space, a closed ball is equivalent to the product of closed balls. More specifically, for any type `β`, function `π` from `β` to another type, where each `b` in `β` has an associated pseudometric space `π b`, and for any nonempty `β`, function `x` from `β` to `π b`, and any real number `r`, the closed ball defined by `x` and `r` is equal to the product of all sets such that each set is the closed ball defined by `x b` and `r` for each `b` in the universal set `β`. Note that a "closed ball" in this context is the set of all points `y` such that the distance from `y` to a given point `x` is less than or equal to a given real number `ε`. More concisely: In a product space of pseudometric spaces indexed by a nonempty type, the closed ball is equal to the product of the closed balls along each index.
`Metric.emetric_closedBall` theorem Metric.emetric_closedBall : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε : ℝ}, 0 ≤ ε → EMetric.closedBall x (ENNReal.ofReal ε) = Metric.closedBall x ε This theorem states that for any pseudo metric space `α`, any point `x` in `α`, and any nonnegative real number `ε`, the closed ball around `x` with extended real number radius `ε` in the extended metric space (`EMetric.closedBall x (ENNReal.ofReal ε)`) is exactly the same as the closed ball around `x` with radius `ε` in the metric space (`Metric.closedBall x ε`). In other words, the closed ball definitions using the distance (`dist`) and the extended distance (`edist`) coincide when the radius is a nonnegative real number. More concisely: For any pseudo-metric space `α`, point `x` in `α`, and nonnegative real number `ε`, the closed balls in the extended metric space with center `x` and radius `ε` (`EMetric.closedBall x (ENNReal.ofReal ε)`) equal the closed balls in the metric space with center `x` and radius `ε` (`Metric.closedBall x ε`).
`Metric.tendstoUniformly_iff` theorem Metric.tendstoUniformly_iff : ∀ {α : Type u} {β : Type v} {ι : Type u_2} [inst : PseudoMetricSpace α] {F : ι → β → α} {f : β → α} {p : Filter ι}, TendstoUniformly F f p ↔ ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ (x : β), dist (f x) (F n x) < ε The theorem `Metric.tendstoUniformly_iff` states that a sequence of functions `F` converges uniformly to a limiting function `f` with respect to a filter `p` if and only if for any positive distance `ε`, eventually with respect to the filter `p`, the distance between `f(x)` and `Fₙ(x)` is less than `ε` for all `x`. This theorem provides a formulation of uniform convergence in terms of the metric or distance function. More concisely: A sequence of functions $F:\mathbb{N} \rightarrow X \rightarrow \mathbb{R}$ uniformly converges to a limit function $f:X \rightarrow \mathbb{R}$ with respect to a filter $p$ if and only if for every $\epsilon > 0$, there exists $N \in \mathbb{N}$ such that for all $x \in X$ and $n \geq N$, we have $\|f(x) - F(x)\| < \epsilon$ for the metric on $X$.
`Metric.inseparable_iff` theorem Metric.inseparable_iff : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x y : α}, Inseparable x y ↔ dist x y = 0 This theorem states that for any two points `x` and `y` in a pseudometric space `α`, `x` and `y` are inseparable (meaning that the neighborhoods of `x` and `y` are identical) if and only if the distance between `x` and `y` is zero. This links the topological concept of inseparability with the metric concept of distance, providing a criterion for inseparability in terms of the distance between the two points. More concisely: In a pseudometric space, two points are inseparable if and only if their distance is zero.
`Metric.closedBall_mem_nhds` theorem Metric.closedBall_mem_nhds : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x : α) {ε : ℝ}, 0 < ε → Metric.closedBall x ε ∈ nhds x This theorem states that for any pseudometric space `α` and any point `x` in `α`, given a real number `ε` greater than 0, the closed ball around `x` with radius `ε` is a member of the neighborhood filter of `x`. In other words, the set of all points `y` with distance to `x` less than or equal to `ε` is a neighborhood of `x`. This makes intuitive sense in metric spaces, where any sufficiently small closed ball around a point can be considered a local neighborhood of that point. More concisely: For any pseudometric space `α` and point `x` in `α`, the closed ball with center `x` and radius `ε` is an element of the neighborhood filter of `x` for any `ε` greater than 0.
`Metric.exists_lt_mem_ball_of_mem_ball` theorem Metric.exists_lt_mem_ball_of_mem_ball : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x y : α} {ε : ℝ}, x ∈ Metric.ball y ε → ∃ ε' < ε, x ∈ Metric.ball y ε' The theorem `Metric.exists_lt_mem_ball_of_mem_ball` states that for any pseudometric space, if a point `x` is within an open ball centered at `y` with radius `ε`, then there exists a strictly smaller radius `ε'` such that `x` is still within the open ball centered at `y` with this smaller radius `ε'`. In other words, if a point is within a certain distance from another point, it will also be within any smaller distance. More concisely: Given a pseudometric space, if a point is in the open ball centered at another point with some radius, then it is also in the open ball centered at the same point with a strictly smaller radius.
`Metric.tendsto_atTop'` theorem Metric.tendsto_atTop' : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : Nonempty β] [inst_2 : SemilatticeSup β] [inst_3 : NoMaxOrder β] {u : β → α} {a : α}, Filter.Tendsto u Filter.atTop (nhds a) ↔ ∀ ε > 0, ∃ N, ∀ n > N, dist (u n) a < ε The theorem `Metric.tendsto_atTop'` states that for any types `α` and `β`, with `α` being a pseudometric space, `β` being nonempty, having a supremum (semilattice), and having no maximum order, and for any function `u : β → α` and any point `a : α`, the function `u` tends towards `a` as `β` tends towards infinity if and only if for every positive real number `ε`, there exists some element `N` in `β` such that for every `n` in `β` greater than `N`, the distance between `u(n)` and `a` is less than `ε`. In mathematical terms, this is saying that limit of function `u` as `β` approaches infinity equals `a` iff for any `ε` greater than zero, there exists an `N` such that for all `n` greater than `N`, the distance between `u(n)` and `a` is less than `ε`. This theorem is a variant of `tendsto_atTop` that uses `n > N` instead of `n ≥ N`. More concisely: For any pseudometric space `α` and a nonempty, suprema-preserving, and boundless set `β`, a function `u : β → α` tends towards `a` in `α` as `β` tends towards infinity if and only if for every `ε > 0`, there exists an `N` in `β` such that `d(u(n), a) < ε` for all `n > N`.
`Mathlib.Topology.MetricSpace.PseudoMetric._auxLemma.65` theorem Mathlib.Topology.MetricSpace.PseudoMetric._auxLemma.65 : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} {a : α}, (a ∈ closure s) = ∀ ε > 0, ∃ b ∈ s, dist a b < ε This theorem states that for any type `α`, which is a pseudometric space, any set `s` of type `α`, and any element `a` of type `α`, the element `a` belongs to the closure of `s` if and only if for every real number `ε` greater than 0, there exists an element `b` in `s` such that the distance between `a` and `b` is less than `ε`. In essence, it's saying that a point is in the closure of a set in a pseudometric space if, for any given positive distance, we can find a point in the set that's less than that distance away. More concisely: In a pseudometric space, an element belongs to the closure of a set if and only if for every positive real number ε, there exists an element in the set within distance ε.
`Metric.tendstoUniformlyOn_iff` theorem Metric.tendstoUniformlyOn_iff : ∀ {α : Type u} {β : Type v} {ι : Type u_2} [inst : PseudoMetricSpace α] {F : ι → β → α} {f : β → α} {p : Filter ι} {s : Set β}, TendstoUniformlyOn F f p s ↔ ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, dist (f x) (F n x) < ε This theorem provides an alternate expression for the uniform convergence of a sequence of functions on a set, using the concept of distance. It says that a sequence of functions `Fₙ` converges uniformly on a set `s` to a limiting function `f` with respect to a filter `p` if and only if, for any positive real number `ε`, there exists a point in the filter `p`, beyond which the distance between the function `f` evaluated at any point `x` in the set `s` and the functions `Fₙ` evaluated at the same point `x`, is less than `ε`. This theorem essentially rephrases the definition of uniform convergence in terms of the distance function `dist`, providing a more intuitive understanding and a practical way to check for uniform convergence. More concisely: A sequence of functions converges uniformly to a limit on a set with respect to a filter if and only if, for every ε > 0, there exists a point in the filter beyond which the distance between the limit function and each function in the sequence at any point is less than ε.
`Metric.ball_eq_empty` theorem Metric.ball_eq_empty : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε : ℝ}, Metric.ball x ε = ∅ ↔ ε ≤ 0 This theorem states that for any type `α` endowed with a pseudo-metric space structure, and for any point `x` of type `α` and a real number `ε`, the metric ball of radius `ε` centered at `x` is empty if and only if `ε` is less than or equal to zero. In mathematical terms, the set of all points `y` such that the distance between `y` and `x` is less than `ε` is empty if and only if `ε` is less than or equal to zero. More concisely: For any pseudo-metric space `(α, d)`, and for all `x ∈ α` and `ε ∈ ℝ`, the open metric ball `{y : α \| d(x, y) < ε}` is empty if and only if `ε ≤ 0`.
`Mathlib.Topology.MetricSpace.PseudoMetric._auxLemma.10` theorem Mathlib.Topology.MetricSpace.PseudoMetric._auxLemma.10 : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x y : α} {ε : ℝ}, (y ∈ Metric.closedBall x ε) = (dist y x ≤ ε) := by sorry This theorem states that for any given type `α` with a pseudometric space structure, any two elements of this type `x` and `y`, and any real number `ε`, `y` is in the closed ball centered at `x` with radius `ε` if and only if the distance between `y` and `x` is less than or equal to `ε`. In other words, the condition for a point `y` to be in the `ε`-closed ball around `x` is equivalent to the condition that the distance from `y` to `x` is at most `ε`. More concisely: For any pseudometric space `(α, d)`, and for all `x ∈ α`, `y ∈ α`, and `ε ∈ ℝ`, `y` is in the closed ball `{z \| d(x, z) ≤ ε}` around `x` if and only if `d(x, y) ≤ ε`.
`Inducing.isSeparable_preimage` theorem Inducing.isSeparable_preimage : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] {f : β → α} [inst_1 : TopologicalSpace β], Inducing f → ∀ {s : Set α}, TopologicalSpace.IsSeparable s → TopologicalSpace.IsSeparable (f ⁻¹' s) This theorem states that if we have a function `f` from a type `β` to another type `α`, where `α` has a structure of a pseudometric space and `β` has a topological space structure, and if `f` is an inducing function, then the preimage of a separable set under `f` is also separable. In other words, if a set `s` in `α` is separable (meaning it can be contained in the closure of a countable set), then the set of all elements in `β` that map into `s` under `f` (denoted `f⁻¹' s`) is also separable. More concisely: If `f` is an inducing function from a topological space `β` to a separable pseudometric space `α`, then the preimage under `f` of any separable set in `α` is separable.
`Mathlib.Topology.MetricSpace.PseudoMetric._auxLemma.8` theorem Mathlib.Topology.MetricSpace.PseudoMetric._auxLemma.8 : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε : ℝ}, (Metric.ball x ε).Nonempty = (0 < ε) The theorem `Mathlib.Topology.MetricSpace.PseudoMetric._auxLemma.8` states that for any type `α` that is equipped with a PseudoMetricSpace structure, and any `x` of type `α` and `ε` of type real numbers (ℝ), the set of all points `y` in the metric ball centered at `x` with radius `ε` is nonempty if and only if `ε` is greater than zero. In simpler terms, it means that a ball in a pseudometric space has points inside it if its radius is positive. More concisely: For any pseudometric space (α, d), and x ∈ α and ε > 0, the metric ball B(x, ε) is nonempty.
`nndist_dist` theorem nndist_dist : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x y : α), nndist x y = (dist x y).toNNReal := by sorry This theorem expresses the non-negative distance (`nndist`) between two points in the context of a pseudometric space in terms of the regular distance (`dist`). More specifically, for any type `α` that forms a PseudoMetricSpace, and for any two points `x` and `y` of type `α`, the non-negative distance between `x` and `y` is equal to the regular distance between `x` and `y` converted to a non-negative real number. More concisely: For any pseudometric space `α` and points `x` and `y` of type `α`, the non-negative distance `nndist x y` between them equals the regular distance `dist x y` converted to a non-negative real number.
`edist_ne_top` theorem edist_ne_top : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x y : α), edist x y ≠ ⊤ This theorem states that in a pseudometric space, the extended distance between any two points is always finite. The pseudometric space is defined over any type `α`. Given any two points `x` and `y` in this space, the theorem guarantees that the extended distance `edist x y` can never be infinite (`⊤`). In mathematical terms, this would be saying that for all points `x` and `y` in a given pseudometric space, the extended distance between `x` and `y` is not equal to infinity. More concisely: In a pseudometric space, the extended distance between any two points is finite.
`Mathlib.Topology.MetricSpace.PseudoMetric._auxLemma.11` theorem Mathlib.Topology.MetricSpace.PseudoMetric._auxLemma.11 : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x y : α} {ε : ℝ}, (y ∈ Metric.sphere x ε) = (dist y x = ε) This theorem, from the PseudoMetric module of the Mathlib Topology MetricSpace library, states that for any type `α` which is equipped with a pseudometric space structure, any two points `x` and `y` of type `α`, and any real number `ε`, the point `y` is in the sphere of radius `ε` centered at `x` if and only if the distance between `y` and `x` is `ε`. This essentially serves as a defining property of the sphere in a pseudometric space. In mathematical terms, we say that a point `y` belongs to the ε-sphere centered at `x` (denoted `Metric.sphere x ε` in lean) if and only if the pseudometric distance from `y` to `x` is exactly `ε`. More concisely: For any pseudometric space `(α, d)`, points `x, y : α`, and real `ε`, `y` belongs to the sphere of radius `ε` around `x` if and only if `d(x, y) = ε`.
`continuous_nndist` theorem continuous_nndist : ∀ {α : Type u} [inst : PseudoMetricSpace α], Continuous fun p => nndist p.1 p.2 This theorem states that for any type `α` that has a `PseudoMetricSpace` structure, the non-negative distance function (`nndist`) is continuous. In other words, given any two points from the type `α`, the function that calculates the non-negative distance between these two points is a continuous function. This is a property that stems from metric spaces, where distances between points vary smoothly. More concisely: For any type `α` equipped with a `PseudoMetricSpace` structure, the non-negative distance function `nndist` is a continuous function.
`Metric.forall_of_forall_mem_closedBall` theorem Metric.forall_of_forall_mem_closedBall : ∀ {α : Type u} [inst : PseudoMetricSpace α] (p : α → Prop) (x : α), (∃ᶠ (R : ℝ) in Filter.atTop, ∀ y ∈ Metric.closedBall x R, p y) → ∀ (y : α), p y The theorem `Metric.forall_of_forall_mem_closedBall` states that for any type `α` equipped with a pseudometric space, for any property `p` of the type, and for any point `x` of the type, if there exists a point in the filter `atTop` (which represents the limit towards infinity) such that the property `p` holds for all points `y` in the closed ball around `x` with radius `R`, then the property `p` holds for all points `y` in the pseudometric space. In other words, if a property holds true for all points in arbitrary large closed balls, then it must hold true for all points in the entire pseudometric space. More concisely: If a property holds for all points in the closed balls of arbitrary radius around a point in a pseudometric space, then the property holds for all points in the pseudometric space.
`closedBall_pi` theorem closedBall_pi : ∀ {β : Type v} {π : β → Type u_3} [inst : Fintype β] [inst_1 : (b : β) → PseudoMetricSpace (π b)] (x : (b : β) → π b) {r : ℝ}, 0 ≤ r → Metric.closedBall x r = Set.univ.pi fun b => Metric.closedBall (x b) r The theorem `closedBall_pi` states that for any type `β`, a function `π` mapping `β` to some type which has a pseudometric space structure, a finitely typed instance of `β`, and a function `x` mapping `β` to the pseudometric space, given a real number `r` greater than or equal to zero, the closed ball in this product space is equivalent to the set of functions (from set `β` to the pseudometric space) such that for each element in `β`, the function maps it into the closed ball in the pseudometric space with the same radius `r`. In mathematical terms, it can be expressed as: for a product of pseudometric spaces, the closed ball centered at a point `x` with radius `r` is the set of all points whose distance to `x` in each individual space does not exceed `r`. More concisely: The closed ball in a product of pseudometric spaces with respect to a point and radius is equivalent to the set of functions mapping each element to a closed ball in the corresponding space with the same radius.
`nndist_pi_le_iff` theorem nndist_pi_le_iff : ∀ {β : Type v} {π : β → Type u_3} [inst : Fintype β] [inst_1 : (b : β) → PseudoMetricSpace (π b)] {f g : (b : β) → π b} {r : NNReal}, nndist f g ≤ r ↔ ∀ (b : β), nndist (f b) (g b) ≤ r The theorem `nndist_pi_le_iff` states that for any given type `β`, a function `π` from `β` to another type, a `Fintype β` instance (which implies β is a finite type), a `PseudoMetricSpace` instance for each `b : β`, and two functions `f` and `g` from `β` to `π b`, the nonnegative real number distance `nndist` between `f` and `g` is less than or equal to a nonnegative real number `r` if and only if the nonnegative real number distance `nndist` between `f b` and `g b` is less than or equal to `r` for every `b` in `β`. This theorem provides an equivalence relation for the inequality of distances in the context of pseudometric spaces. More concisely: For any finite type β, function π from β to another type, PseudoMetricSpace instances for each element b in β, and functions f and g from β to π b, the distance nndist(f, g) ≤ r if and only if nndist(fb, gb) ≤ r for all b in β.
`ContinuousOn.isSeparable_image` theorem ContinuousOn.isSeparable_image : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α}, ContinuousOn f s → TopologicalSpace.IsSeparable s → TopologicalSpace.IsSeparable (f '' s) This theorem states that if a function `f` is continuous on a separable set `s` in a pseudometric space, then the image of `s` under the function `f` is also a separable set in its topological space. Here, a set is considered 'separable' if it is contained within the closure of a countable set. The continuity of a function on a set is defined as the function being continuous at every point within the set. More concisely: If a continuous function maps a separable set in a pseudometric space to a set that is contained in the closure of a countable set, then the image set is separable.
`squeeze_zero'` theorem squeeze_zero' : ∀ {α : Type u_3} {f g : α → ℝ} {t₀ : Filter α}, (∀ᶠ (t : α) in t₀, 0 ≤ f t) → (∀ᶠ (t : α) in t₀, f t ≤ g t) → Filter.Tendsto g t₀ (nhds 0) → Filter.Tendsto f t₀ (nhds 0) This theorem, often known as the Squeeze Theorem, relates to the limit of a real-valued function `f` at a point in its domain under a filter `t₀`. The theorem states that if, for every `t` in the domain of `f` and `g` such that `t` is in the neighborhood of `t₀`, the value of `f(t)` is greater than or equal to 0 and less than or equal to `g(t)`, and if the function `g` tends to 0 as `t` approaches `t₀`, then the function `f` also tends to 0 as `t` approaches `t₀`. This is a special case of the more general Sandwich Theorem. More concisely: If a real-valued function `f` is sandwiched between a positive function `g` that tends to 0 at a point `t₀`, then `f` also tends to 0 at `t₀`. (Squeeze Theorem)
`dist_self` theorem dist_self : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x : α), dist x x = 0 This theorem states that for any type `α` that is a `PseudoMetricSpace`, the distance of any element `x` from itself is `0`. In mathematical terms, for a given element in a pseudo-metric space, the distance between the element and itself is always zero. This is consistent with the fundamental property of metric spaces where the distance from a point to itself is always zero. More concisely: For any pseudo-metric space `α`, the distance of any element `x` from itself is `0`. (or equivalently, `d x x = 0` where `d` is the distance function)
`Metric.uniformity_eq_comap_nhds_zero` theorem Metric.uniformity_eq_comap_nhds_zero : ∀ {α : Type u} [inst : PseudoMetricSpace α], uniformity α = Filter.comap (fun p => dist p.1 p.2) (nhds 0) := by sorry The theorem `Metric.uniformity_eq_comap_nhds_zero` states that for any type `α` that has a `PseudoMetricSpace` structure, the uniformity on `α` is equal to the preimage (comap) under the distance function (where the distance function maps a pair of points to the distance between them) of the neighborhood filter at 0. In other words, the uniformity filter on `α` can be constructed by taking the set of all pairs of points whose distance falls within some neighborhood of zero. This theorem is crucial in linking the concepts of the uniformity and the topology in a pseudometric space. More concisely: The uniformity on a PseudoMetricSpace equals the preimage under the distance function of the neighborhood filter at 0.
`squeeze_zero` theorem squeeze_zero : ∀ {α : Type u_3} {f g : α → ℝ} {t₀ : Filter α}, (∀ (t : α), 0 ≤ f t) → (∀ (t : α), f t ≤ g t) → Filter.Tendsto g t₀ (nhds 0) → Filter.Tendsto f t₀ (nhds 0) The `squeeze_zero` theorem is a special variant of the squeeze theorem. In the context of real-valued functions `f` and `g` and a filter `t₀` on an arbitrary type `α`, the theorem states that if `f` is always non-negative and never exceeds `g`, and if `g` converges to zero along the filter `t₀`, then `f` also converges to zero along `t₀`. In other words, if `0 ≤ f(t) ≤ g(t)` for all `t` in `α`, and `g` tends towards zero as `t` approaches `t₀`, then `f` will also tend towards zero. More concisely: If `f(t)` is a non-negative real-valued function that is pointwise bounded above by another function `g(t)` that converges to zero along a filter `t₀`, then `f(t)` converges to zero along `t₀`.
`edist_lt_top` theorem edist_lt_top : ∀ {α : Type u_3} [inst : PseudoMetricSpace α] (x y : α), edist x y < ⊤ This theorem states that in a pseudometric space, the extended distance between any two points is always finite. Specifically, for any type `α` that forms a pseudometric space (as indicated by the assumption `[inst : PseudoMetricSpace α]`), and for any two elements `x` and `y` of `α`, the extended distance `edist x y` is less than infinity (`< ⊤`). This captures the idea that no matter which two points you pick in a pseudometric space, you can always assign a meaningful, finite distance between them. More concisely: In a pseudometric space, the extended distance between any two points is finite.
`Metric.closedBall_diff_ball` theorem Metric.closedBall_diff_ball : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε : ℝ}, Metric.closedBall x ε \ Metric.ball x ε = Metric.sphere x ε The theorem `Metric.closedBall_diff_ball` asserts that for any pseudometric space `α`, any point `x` in `α`, and any real number `ε`, the difference between the closed ball centered at `x` with radius `ε` and the open ball centered at `x` with radius `ε` equals the sphere centered at `x` with radius `ε`. In other words, it removes all points within a distance less than `ε` from `x` from the set of points within a distance less than or equal to `ε` from `x`, leaving only the set of points exactly `ε` distance from `x`. More concisely: The theorem asserts that in a pseudometric space, the difference between the closed and open balls centered at a point with equal radius is equal to the sphere centered at that point.
`nndist_self` theorem nndist_self : ∀ {α : Type u} [inst : PseudoMetricSpace α] (a : α), nndist a a = 0 This theorem states that for any point in a pseudo metric space, the non-negative distance of the point to itself is always zero. Here, `nndist a a` denotes the non-negative distance from point `a` to itself in the pseudo metric space `α`. The theorem holds for any type `α` that has a pseudo metric space structure. More concisely: For any point in a pseudo metric space, its non-negative distance to itself is equal to zero.
`tendsto_iff_dist_tendsto_zero` theorem tendsto_iff_dist_tendsto_zero : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] {f : β → α} {x : Filter β} {a : α}, Filter.Tendsto f x (nhds a) ↔ Filter.Tendsto (fun b => dist (f b) a) x (nhds 0) The theorem `tendsto_iff_dist_tendsto_zero` states that for any function `f` from a type `β` to a type `α` where `α` has a pseudometric space structure, a filter `x` on `β` and a point `a` in `α`, the function `f` tends to `a` with respect to the filter `x` if and only if the distance between `f` and `a` tends to zero with respect to the same filter `x`. This is essentially saying that the limit of a function at a point in a pseudometric space is equivalent to the distance from the function to the point converging to zero. More concisely: A function from a pseudometric space to itself tends to a point if and only if the distance between the function and the point converges to zero with respect to the given filter.
`Metric.isOpen_ball` theorem Metric.isOpen_ball : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε : ℝ}, IsOpen (Metric.ball x ε) := by sorry The theorem `Metric.isOpen_ball` states that for any type `α` that is a pseudometric space, and for any point `x` in `α` and any real number `ε`, the metric ball centered at `x` with radius `ε` is an open set in the topological space of `α`. In mathematical terms, this is saying that the set of all points `y` such that the distance between `y` and `x` is less than `ε` is an open set. This is a fundamental property of metric spaces in topology. More concisely: In a pseudometric space, the metric ball centered at a point is an open set.
`Metric.mem_ball` theorem Metric.mem_ball : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x y : α} {ε : ℝ}, y ∈ Metric.ball x ε ↔ dist y x < ε This theorem, named `Metric.mem_ball`, states that for any pseudometric space `α` and any elements `x` and `y` of `α`, along with a real number `ε`, the element `y` belongs to the ball of radius `ε` centered at `x` if and only if the distance from `y` to `x` is less than `ε`. In mathematical terms, this states that $y \in B(x, \epsilon)$ if and only if $d(y, x) < \epsilon$, where $B(x, \epsilon)$ represents the ball of radius $\epsilon$ centered at $x$ and $d(y, x)$ represents the distance from `y` to `x` in the pseudometric space. More concisely: For any pseudometric space and elements, an element belongs to the ball of radius ε centered at another element if and only if the distance between them is less than ε.
`Metric.emetric_ball_nnreal` theorem Metric.emetric_ball_nnreal : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε : NNReal}, EMetric.ball x ↑ε = Metric.ball x ↑ε This theorem states that in any pseudometric space (a generalization of metric spaces), the concept of an "ε-ball" centered at a point 'x', defined using either the extended distance (edistance) or the usual distance, are the same. An ε-ball is a set of all points 'y' whose (e)distance from 'x' is less than ε. Here, ε is a nonnegative real number. The theorem essentially asserts that both definitions of balls coincide in such spaces. More concisely: In any pseudometric space, the sets of points with extended distance and usual distance less than ε from a given point form identical ε-balls.
`ball_pi'` theorem ball_pi' : ∀ {β : Type v} {π : β → Type u_3} [inst : Fintype β] [inst_1 : (b : β) → PseudoMetricSpace (π b)] [inst_2 : Nonempty β] (x : (b : β) → π b) (r : ℝ), Metric.ball x r = Set.univ.pi fun b => Metric.ball (x b) r The theorem `ball_pi'` states that, for any type `β`, any function `π` from `β` to some other type, given that `β` is finite and every type `π b` is a pseudo metric space, and there exists at least one element in `β`, for any function `x` from `β` to each `π b` and any real number `r`, an open ball in the product space of `β` and `π` is equivalent to the product of open balls in each `π b`. In other words, the set of all points in the product space that are less than `r` distance from `x` is equivalent to the set of all points in each space `π b` that are less than `r` distance from `x(b)`. More concisely: Given a finite type `β` and a function `π:` `β` → Type, where each `π b` is a pseudo metric space, the open ball in the product space `β × (π := Π b, π b)` centered at `(x: β) × (x₀: Π b, π b)` with radius `r` is equivalent to the product of open balls in each `π b` centered at `x b` with radius `r`.
`edist_nndist` theorem edist_nndist : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x y : α), edist x y = ↑(nndist x y) This theorem states that for any pseudometric space `α` and any two elements `x` and `y` in this space, the extended distance `edist` between `x` and `y` equals the non-negative real number equivalent (`↑`) of the non-negative distance `nndist` between `x` and `y`. In other words, in any pseudometric space, the `edist` function is essentially the same as the `nndist` function, but expressed in the extended real number system. More concisely: In any pseudometric space, the extended distance between two elements equals the non-negative distance's non-negative real number equivalent. Or, using Lean's notation: `for any α : Type, (α => ℝ) => is_pseudometric α → ∀ x y : α, edist x y = ⇑(nndist x y)`
`dist_nndist` theorem dist_nndist : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x y : α), dist x y = ↑(nndist x y) This theorem, `dist_nndist`, states that for any given pseudometric space `α`, and any two elements `x` and `y` in this space, the `dist` function between `x` and `y` is equivalent to the non-negative real number (`↑`) representation of the `nndist` (non-negative distance) function between `x` and `y`. This theorem essentially relates the traditional distance measure in a pseudometric space to its non-negative counterpart. More concisely: For any pseudometric space, the distance between two elements is equivalent to the non-negative representation of their nested neighborhood distance.
`dist_dist_dist_le_left` theorem dist_dist_dist_le_left : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x y z : α), dist (dist x z) (dist y z) ≤ dist x y This theorem states that for any pseudometric space (a set equipped with a function that measures distances between elements of the set) and for any three elements within that space (x, y, and z), the absolute difference between the distance from x to z and the distance from y to z is less than or equal to the distance from x to y. More concisely: For any pseudometric space and elements x, y, z in it, \|d(x, z) - d(y, z)\| ≤ d(x, y), where d is the distance function.
`Real.ball_eq_Ioo` theorem Real.ball_eq_Ioo : ∀ (x r : ℝ), Metric.ball x r = Set.Ioo (x - r) (x + r) The theorem `Real.ball_eq_Ioo` states that for all real numbers `x` and `r`, the open ball centered at `x` with radius `r` (which is the set of all points `y` such that the distance from `y` to `x` is less than `r`) is equal to the open interval from `x - r` to `x + r`, excluding the endpoints. In other words, in the real numbers, the set of points `y` satisfying `\|y - x\| < r` is exactly those in the interval `(x - r, x + r)`. More concisely: The open ball centered at real number `x` with radius `r` equals the open interval `(x - r, x + r)` in the real numbers.
`Metric.ball_union_sphere` theorem Metric.ball_union_sphere : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε : ℝ}, Metric.ball x ε ∪ Metric.sphere x ε = Metric.closedBall x ε This theorem, `Metric.ball_union_sphere`, states that for any type `α` that is equipped with a `PseudoMetricSpace` structure, and for any point `x` of type `α` and any real number `ε`, the union of the open ball centered at `x` with radius `ε` and the sphere centered at `x` with radius `ε` is equal to the closed ball centered at `x` with radius `ε`. In mathematical terms, this means that if you take all points `y` such that the distance from `y` to `x` is less than `ε` (which forms the open ball) and add the set of all points `y` such that the distance from `y` to `x` equals `ε` (which forms the sphere), you get the set of all points `y` such that the distance from `y` to `x` is less than or equal to `ε` (which forms the closed ball). More concisely: For any `PseudoMetricSpace` `α` and point `x` in `α` with real number `ε`, the closed ball centered at `x` with radius `ε` equals the union of the open ball centered at `x` with radius `ε` and the sphere centered at `x` with radius `ε`.
`nndist_comm` theorem nndist_comm : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x y : α), nndist x y = nndist y x This theorem states that in any pseudometric space (a mathematical space where distance between points is defined), the non-negative distance (`nndist`) between two points `x` and `y` is the same regardless of the order in which the points are considered. In other words, the non-negative distance from `x` to `y` is the same as the non-negative distance from `y` to `x`. This is a reflection of the commutative property of distance in pseudometric spaces. More concisely: In any pseudometric space, the non-negative distance between two points is commutative, i.e., `nndist x y = nndist y x`.
`Metric.eventually_prod_nhds_iff` theorem Metric.eventually_prod_nhds_iff : ∀ {α : Type u} {ι : Type u_2} [inst : PseudoMetricSpace α] {f : Filter ι} {x₀ : α} {p : ι × α → Prop}, (∀ᶠ (x : ι × α) in f ×ˢ nhds x₀, p x) ↔ ∃ pa, (∀ᶠ (i : ι) in f, pa i) ∧ ∃ ε > 0, ∀ {i : ι}, pa i → ∀ {x : α}, dist x x₀ < ε → p (i, x) The theorem `Metric.eventually_prod_nhds_iff` states that, for any pseudometric space `α`, any filter `f` on a type `ι`, any point `x₀` in `α`, and any property `p` on the product of `ι` and `α`, the property `p` holds eventually in the product filter of `f` and the neighborhood filter of `x₀` if and only if there exists a property `pa` on `ι` such that `pa` holds eventually in `f`, and there exists a positive real number `ε` such that for all `i` in `ι` for which `pa` holds and for all `x` in `α` with distance less than `ε` from `x₀`, the property `p` holds on the pair `(i, x)`. More concisely: A property `p` on the product of a filter `f` on `ι` and a pseudometric space `α` holds eventually in the product filter of `f` and the neighborhood filter of a point `x₀` if and only if there exists a property `pa` on `ι` holding eventually in `f` and a positive real number `ε` such that `p` holds on `(i, x)` for all `i` satisfying `pa` and all `x` with distance to `x₀` less than `ε`.
`Metric.nonempty_ball` theorem Metric.nonempty_ball : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε : ℝ}, (Metric.ball x ε).Nonempty ↔ 0 < ε The theorem `Metric.nonempty_ball` states that in any pseudometric space, a ball of radius `ε` centered at a point `x` is not empty if and only if `ε` is greater than zero. In other words, there is at least one point `y` such that the distance from `y` to `x` is less than `ε`, if and only if `ε` is positive. Here, `dist y x < ε` defines the metric ball, and `Set.Nonempty (Metric.ball x ε)` means the set of all such points `y` is nonempty. More concisely: In a pseudometric space, the metric ball centered at a point with positive radius is nonempty.
`Metric.exists_ball_inter_eq_singleton_of_mem_discrete` theorem Metric.exists_ball_inter_eq_singleton_of_mem_discrete : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} [inst_1 : DiscreteTopology ↑s] {x : α}, x ∈ s → ∃ ε > 0, Metric.ball x ε ∩ s = {x} This theorem states that for any given point `x` in a discrete subset `s` of a pseudometric space, there exists an open ball centered at `x` which intersects with the set `s` only at the point `x`. This means that within a certain positive distance `ε` (for which the open ball is defined), no other points in `s` are present except `x`. The existence of such an open ball is a property of discrete sets in pseudometric spaces. More concisely: For any discrete subset `s` of a pseudometric space and any point `x` in `s`, there exists an open ball centered at `x` that contains only `x` from `s`.
`dist_edist` theorem dist_edist : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x y : α), dist x y = (edist x y).toReal This theorem states that for any type `α` that is a pseudo-metric space, the distance `dist` between any two elements `x` and `y` of `α` is equal to the real number representation (`.toReal`) of the extended distance `edist` between `x` and `y`. In simpler terms, it links the concepts of distance and extended distance in a pseudo-metric space, stating that they are essentially the same, but represented in different ways (standard vs extended, or real numbers vs extended real numbers). More concisely: For any pseudo-metric space `α` and elements `x` and `y` in `α`, `dist x y` equals the real number representation of the extended distance `edist x y`.
`dist_le_Ico_sum_of_dist_le` theorem dist_le_Ico_sum_of_dist_le : ∀ {α : Type u} [inst : PseudoMetricSpace α] {f : ℕ → α} {m n : ℕ}, m ≤ n → ∀ {d : ℕ → ℝ}, (∀ {k : ℕ}, m ≤ k → k < n → dist (f k) (f (k + 1)) ≤ d k) → dist (f m) (f n) ≤ (Finset.Ico m n).sum fun i => d i This theorem, `dist_le_Ico_sum_of_dist_le`, states that in a pseudo metric space `α`, for any function `f` from natural numbers to `α`, and for any two natural numbers `m` and `n` such that `m` is less than or equal to `n`, if for every natural number `k` between `m` and `n` (exclusive), the distance 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 `d(i)` for each `i` in the finite set of natural numbers from `m` to `n` (including `m` but excluding `n`). Essentially, the total distance from `f(m)` to `f(n)` is bounded above by the sum of the upper estimates for each individual step from `f(k)` to `f(k+1)`. More concisely: In a pseudo metric space, given a function from natural numbers to the space and natural numbers m <= n, if the distance between successive function values is less than or equal to the given distance d(i) for all i from m to n-1, then the distance between the function values at m and n is less than or equal to the sum of the distances d(i) from m to n.
`Metric.uniformity_basis_dist` theorem Metric.uniformity_basis_dist : ∀ {α : Type u} [inst : PseudoMetricSpace α], (uniformity α).HasBasis (fun ε => 0 < ε) fun ε => {p \| dist p.1 p.2 < ε} The theorem `Metric.uniformity_basis_dist` states that for any type `α` that is a `PseudoMetricSpace`, the uniformity (which is a filter on the product space `α × α`) has a basis consisting of sets of pairs `(x, y)` where the distance `dist` between `x` and `y` is less than some positive real number `ε`. This means that any set in the uniformity can be generated as a union of these basic sets, and these sets themselves are indexed by the positive real numbers. This provides a bridge between the abstract uniformity filter and the concrete metric `dist`. More concisely: For any PseudoMetricSpace `α`, the basis of its uniformity consists of sets of pairs `(x, y)` with distance `dist(x, y)` less than some positive real `ε`.
`Metric.emetric_ball_top` theorem Metric.emetric_ball_top : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x : α), EMetric.ball x ⊤ = Set.univ := by sorry The theorem `Metric.emetric_ball_top` states that for any type `α` that is a PseudoMetricSpace and any point `x` of type `α`, the extended metric ball with center `x` and radius `∞` (represented by `EMetric.ball x ⊤`) is equal to the universal set (`Set.univ`). In other words, the set of all points whose extended distance from `x` is less than infinity includes every point in the space, i.e., it is the universal set. More concisely: For any PseudoMetricSpace `α` and point `x` in `α`, the extended metric ball `EMetric.ball x ⊤` equals the universal set `Set.univ`. In other words, every point in `α` is within infinite distance from `x`.
`Metric.exists_closedBall_inter_eq_singleton_of_discrete` theorem Metric.exists_closedBall_inter_eq_singleton_of_discrete : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} [inst_1 : DiscreteTopology ↑s] {x : α}, x ∈ s → ∃ ε > 0, Metric.closedBall x ε ∩ s = {x} The theorem `Metric.exists_closedBall_inter_eq_singleton_of_discrete` states that for any point `x` in a discrete subset `s` of a pseudometric space, there exists a closed ball with a positive radius centered at `x` that intersects the subset `s` only at the point `x`. In more mathematical terms, given a pseudometric space `α`, a discrete subset `s` of `α`, and a point `x` in `s`, there exists a real number `ε` greater than 0 such that the intersection of the closed ball centered at `x` with radius `ε` and the subset `s` is a singleton set containing only `x`. This essentially means that in a discrete topology, we can isolate any given point in a subset with a small enough closed ball. More concisely: For any discrete subset `s` of a pseudometric space `α` and any point `x` in `s`, there exists a positive radius `ε` such that the closed ball centered at `x` with radius `ε` intersects `s` only at `x`.
`lebesgue_number_lemma_of_metric` theorem lebesgue_number_lemma_of_metric : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} {ι : Sort u_3} {c : ι → Set α}, IsCompact s → (∀ (i : ι), IsOpen (c i)) → s ⊆ ⋃ i, c i → ∃ δ > 0, ∀ x ∈ s, ∃ i, Metric.ball x δ ⊆ c i The Lebesgue number lemma for a metric space is stated as follows: for any metric space `α`, any compact set `s` within that space, and any indexed collection `{c i}` of open sets, if the set `s` is covered by the union of these open sets, then there exists a positive real number `δ` such that for every point `x` in the set `s`, there is an index `i` such that the open ball of radius `δ` centered at `x` is a subset of the open set `c i`. In other words, `δ` is a measure of the "size" of the open sets in the cover relative to the set `s` they are covering. More concisely: For any compact set in a metric space and any open cover, there exists a positive number δ such that for each point in the set, there is an open set in the cover containing a ball of radius δ around that point.
`Metric.closedBall_subset_ball` theorem Metric.closedBall_subset_ball : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε₁ ε₂ : ℝ}, ε₁ < ε₂ → Metric.closedBall x ε₁ ⊆ Metric.ball x ε₂ The theorem `Metric.closedBall_subset_ball` states that for any type `α` that is a pseudo metric space, for any point `x` of type `α`, and for any two real numbers `ε₁` and `ε₂`, if `ε₁` is less than `ε₂`, then the closed ball centered at `x` with radius `ε₁` is a subset of the open ball centered at `x` with radius `ε₂`. In other words, all points `y` at a distance from `x` less than or equal to `ε₁` (forming a closed ball around `x`) are also at a distance from `x` less than `ε₂` (thus falling within an open ball around `x`). More concisely: For any pseudo metric space `α` and point `x` in `α`, the closed ball `Bcl(x, ε₁)` is a subset of the open ball `Bop(x, ε₂)` when `ε₁` is less than `ε₂`.
`Metric.mem_closedBall'` theorem Metric.mem_closedBall' : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x y : α} {ε : ℝ}, y ∈ Metric.closedBall x ε ↔ dist x y ≤ ε This theorem states that for any pseudometric space `α`, any two points `x` and `y` in `α`, and any real number `ε`, `y` is in the closed ball centered at `x` with radius `ε` if and only if the distance from `x` to `y` is less than or equal to `ε`. In other words, it provides a condition for a point's membership in the closed ball in terms of the pseudometric distance. More concisely: For any pseudometric space and points x, y, the closed ball with center x and radius ε contains y if and only if the distance from x to y is less than or equal to ε.
`tendsto_of_tendsto_of_dist` theorem tendsto_of_tendsto_of_dist : ∀ {α : Type u} {ι : Type u_2} [inst : PseudoMetricSpace α] {f₁ f₂ : ι → α} {p : Filter ι} {a : α}, Filter.Tendsto f₁ p (nhds a) → Filter.Tendsto (fun x => dist (f₁ x) (f₂ x)) p (nhds 0) → Filter.Tendsto f₂ p (nhds a) This theorem, referred to as an alias of `Filter.Tendsto.congr_dist`, states the following: given any types `α` and `ι`, with `α` being a pseudo metric space, and given any two functions `f₁` and `f₂` from `ι` to `α`, a filter `p` on `ι`, and a point `a` in `α`, if the function `f₁` tends to the neighborhood filter at `a` under filter `p`, and the distance between the images of `f₁` and `f₂` under any `x` from the domain tends to the neighborhood filter at `0` under the filter `p`, then the function `f₂` also tends to the neighborhood filter at `a` under the filter `p`. In simpler terms, if `f₁` converges to `a` and `f₁` and `f₂` become arbitrarily close, then `f₂` also converges to `a`. More concisely: If `f₁` tends to `a` in the filter `p` and the distance between `f₁(x)` and `f₂(x)` tends to 0 in the filter `p` for all `x`, then `f₂` tends to `a` in the filter `p`.
`eventually_closedBall_subset` theorem eventually_closedBall_subset : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {u : Set α}, u ∈ nhds x → ∀ᶠ (r : ℝ) in nhds 0, Metric.closedBall x r ⊆ u The theorem `eventually_closedBall_subset` states that for any type `α` with a pseudometric space structure, any point `x` of type `α`, and any set `u` of type `α`, if `u` is a neighborhood of `x`, then there exists a neighborhood of `0` in the real numbers, such that for all `r` in this neighborhood, the closed ball centered at `x` with radius `r` (represented by `Metric.closedBall x r` and defined as the set of all points `y` where the distance between `y` and `x` is less than or equal to `r`) is a subset of `u`. This essentially means that for small enough `r`, the closed ball `Metric.closedBall x r` is contained in `u`. More concisely: For any pseudometric space `(α, d)` and point `x ∈ α`, if `u ⊆ α` is a neighborhood of `x`, then there exists a real number `r > 0` such that `Metric.closedBall x r ⊆ u`.
`Mathlib.Topology.MetricSpace.PseudoMetric._auxLemma.66` theorem Mathlib.Topology.MetricSpace.PseudoMetric._auxLemma.66 : ∀ {α : Type u_1} {ι : Sort u_4} {f : ι → α} {p : α → Prop}, (∃ a ∈ Set.range f, p a) = ∃ i, p (f i) This theorem states that for any type `α` and any sort `ι`, if we have a function `f` mapping `ι` to `α` and a property `p` that an element of `α` might satisfy, then there exists an element `a` in the range of `f` that satisfies `p` if and only if there exists an `i` such that the application of `f` to `i` satisfies `p`. Essentially, it says that an element in the range of `f` satisfies a property if and only if the element is the image of some input under `f` that satisfies the property. More concisely: For any function `f` from sort `ι` to type `α`, and property `p` on `α`, the existence of an `i` in `ι` such that `f i` satisfies `p` is equivalent to the existence of an `a` in the range of `f` that satisfies `p`.
`Metric.tendstoLocallyUniformlyOn_iff` theorem Metric.tendstoLocallyUniformlyOn_iff : ∀ {α : Type u} {β : Type v} {ι : Type u_2} [inst : PseudoMetricSpace α] [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, dist (f y) (F n y) < ε The theorem `Metric.tendstoLocallyUniformlyOn_iff` states that a sequence of functions `F : ι → β → α` converges locally uniformly to a function `f : β → α` on a set `s` if and only if, for any positive real number `ε` and any point `x` in the set `s`, there exists a neighborhood `t` within `s` around `x` such that, for all sufficiently large `n` (in the sense of the filter `p`), the distance between `f(y)` and `F n y` is less than `ε` for all `y` in `t`. Here, `α` is a type with a pseudometric space structure, `β` is a type with a topological space structure, and `ι` indexes the sequence of functions. More concisely: A sequence of functions `F : ι → β → α` converges locally uniformly to `f : β → α` on a set `s` if and only if for every `ε > 0` and `x ∈ s`, there exists a neighborhood `t` of `x` such that, for all large enough `n`, the pseudometric distance between `f(y)` and `F n y` is less than `ε` for all `y ∈ t`.
`Metric.mk_uniformity_basis_le` theorem Metric.mk_uniformity_basis_le : ∀ {α : Type u} [inst : PseudoMetricSpace α] {β : Type u_3} {p : β → Prop} {f : β → ℝ}, (∀ (x : β), p x → 0 < f x) → (∀ (ε : ℝ), 0 < ε → ∃ x, p x ∧ f x ≤ ε) → (uniformity α).HasBasis p fun x => {p \| dist p.1 p.2 ≤ f x} The theorem `Metric.mk_uniformity_basis_le` states that for a given function `f` from some type `β` to the real numbers, if `f` maps the set `{i \| p i}` to a set of positive real numbers that accumulate to zero, then the closed neighborhoods of the diagonal of some pseudometric space `α` of sizes `{f i \| p i}` form a basis of the uniformity of `α`. This theorem is used to establish specific bases for the uniformity, such as `uniformity_basis_dist_le`. Additional bases can be added easily in the future if needed. More concisely: If a function from a type to the positive real numbers with the property that the set of images of elements satisfying a given property covers the diagonal of a pseudometric space forms a collection of neighborhood sizes, then this collection is a basis for the uniformity of the pseudometric space.
`Metric.mem_ball'` theorem Metric.mem_ball' : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x y : α} {ε : ℝ}, y ∈ Metric.ball x ε ↔ dist x y < ε The theorem `Metric.mem_ball'` states that for any type `α` equipped with a pseudo metric space structure, any points `x` and `y` of type `α`, and any real number `ε`, `y` is in the ball of radius `ε` centered at `x` (denoted as `Metric.ball x ε`) if and only if the distance between `x` and `y` is less than `ε`. In mathematical terms, this means `y ∈ B(x, ε)` if and only if `d(x, y) < ε`, where `B(x, ε)` is the open ball centered at `x` with radius `ε`, and `d(x, y)` is the distance between `x` and `y`. More concisely: For any pseudo metric space (α, d), and points x, y in α, y belongs to the open ball B(x, ε) if and only if the distance d(x, y) < ε.
`Continuous.dist` theorem Continuous.dist : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : TopologicalSpace β] {f g : β → α}, Continuous f → Continuous g → Continuous fun b => dist (f b) (g b) This theorem states that for any two given functions `f` and `g` mapping from a topological space `β` to a pseudo-metric space `α`, if both `f` and `g` are continuous, then the function that maps `b` in `β` to the distance between `f(b)` and `g(b)` in `α` is also continuous. In mathematical terms, if $f$ and $g$ are continuous functions from a topological space to a pseudo-metric space, then the function $h(b) = \mathrm{dist}(f(b), g(b))$ is also continuous. More concisely: If `f` and `g` are continuous functions from a topological space to a pseudo-metric space, then the function mapping the distance between `f(x)` and `g(x)` is also continuous.
`dist_le_pi_dist` theorem dist_le_pi_dist : ∀ {β : Type v} {π : β → Type u_3} [inst : Fintype β] [inst_1 : (b : β) → PseudoMetricSpace (π b)] (f g : (b : β) → π b) (b : β), dist (f b) (g b) ≤ dist f g This theorem states that for any type `β`, and any type `π` which is a function of `β`, if `β` is a finite type and for all `b` in `β`, `π b` forms a pseudo metric space, then for any two functions `f` and `g` from `β` to `π b`, the distance between `f(b)` and `g(b)` for any `b` in `β` is less than or equal to the distance between the functions `f` and `g` themselves. This is a generalization of the property that the distance between two points is always less than the distance between the paths connecting them. More concisely: For any finite type `β` and type `π` being a function of `β`, if for each `b` in `β`, `π b` forms a pseudo metric space, then for all functions `f` and `g` from `β` to `π b`, the pointwise distance between `f(b)` and `g(b)` is less than or equal to the uniform distance between `f` and `g`.
`nndist_edist` theorem nndist_edist : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x y : α), nndist x y = (edist x y).toNNReal := by sorry This theorem, `nndist_edist`, expresses the non-negative distance (`nndist`) between two points `x` and `y` in a pseudo metric space `α` in terms of the extended real distance (`edist`). Essentially, it states that for any two points in a pseudo metric space, the non-negative distance is equal to the extended real distance converted to a non-negative real number. More concisely: For any pseudo metric space and any two of its points, the non-negative distance between them equals the extended real distance between them in absolute value.
`Metric.tendstoUniformlyOnFilter_iff` theorem Metric.tendstoUniformlyOnFilter_iff : ∀ {α : Type u} {β : Type v} {ι : Type u_2} [inst : PseudoMetricSpace α] {F : ι → β → α} {f : β → α} {p : Filter ι} {p' : Filter β}, TendstoUniformlyOnFilter F f p p' ↔ ∀ ε > 0, ∀ᶠ (n : ι × β) in p ×ˢ p', dist (f n.2) (F n.1 n.2) < ε This theorem states that a sequence of functions `F` converges uniformly to a limiting function `f` with respect to filters `p` and `p'`, if and only if for all positive real numbers `ε`, eventually for each pair `(n, b)` in the cartesian product of filters `p` and `p'`, the distance between `f(b)` and `F(n, b)` is less than `ε`. In other words, this theorem provides a way to express the uniform convergence of a sequence of functions in terms of the metric space notion of distance. More concisely: A sequence of functions `F` uniformly converges to `f` with respect to filters `p` and `p'` if and only if for all `ε > 0`, there exists an index `N` such that for all pairs `(n, b)` in the product of `p` and `p'`, `\|f(b) - F(n, b)\| < ε`.
`Real.closedBall_eq_Icc` theorem Real.closedBall_eq_Icc : ∀ {x r : ℝ}, Metric.closedBall x r = Set.Icc (x - r) (x + r) The theorem `Real.closedBall_eq_Icc` states that for any real numbers `x` and `r`, the closed ball centered at `x` with radius `r` in the real numbers, which is the set of all points `y` such that the distance between `y` and `x` is less than or equal to `r`, is equal to the closed interval from `x - r` to `x + r`. In mathematical terms, it asserts that for all real numbers `x` and `r`, we have `Metric.closedBall x r = [x - r, x + r]`. More concisely: The theorem `Real.closedBall_eq_Icc` asserts that for all real numbers `x` and `r`, the closed ball centered at `x` with radius `r` equals the closed interval `[x-r, x+r]` in the real numbers.
`Metric.isClosed_sphere` theorem Metric.isClosed_sphere : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε : ℝ}, IsClosed (Metric.sphere x ε) The theorem `Metric.isClosed_sphere` states that for any given type `α` that has a `PseudoMetricSpace` structure, any point `x` of type `α`, and any real number `ε`, the sphere centered at `x` with radius `ε` is a closed set. Here, a 'sphere' is defined as the set of all points `y` such that the distance between `y` and `x` is equal to `ε`. The concept of 'closed set' is defined per the topology induced by the pseudometric on `α`. More concisely: For any type `α` with a `PseudoMetricSpace` structure and any `x : α` and real `ε`, the sphere centered at `x` with radius `ε` is a closed set in the topology induced by the pseudometric on `α`.
`Filter.Tendsto.dist` theorem Filter.Tendsto.dist : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] {f g : β → α} {x : Filter β} {a b : α}, Filter.Tendsto f x (nhds a) → Filter.Tendsto g x (nhds b) → Filter.Tendsto (fun x => dist (f x) (g x)) x (nhds (dist a b)) This theorem states that for any two functions `f` and `g` from a type `β` to a pseudometric space `α`, if `f` tends to `a` and `g` tends to `b` (for some `a, b` in `α`) as `x` varies in a filter `x`, then the distance between `f(x)` and `g(x)` also tends to the distance between `a` and `b`. In other words, as we get closer to `x` in the filter, the distance between the images of `x` under `f` and `g` approaches the distance between `a` and `b`. This theorem relates the notion of convergence in pseudometric spaces with the notion of convergence in filters. More concisely: Given functions `f` and `g` from a filter `x` on type `β` to a pseudometric space `α`, if `f x` converges to `a` and `g x` converges to `b`, then `distance(a, b) ≤ limit-inf (distance(f x, g x))`.
`abs_dist_sub_le` theorem abs_dist_sub_le : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x y z : α), \|dist x z - dist y z\| ≤ dist x y This theorem states that for any type `α` that is a pseudometric space, and for any three points `x`, `y`, and `z` in this space, the absolute difference between the distance from `x` to `z` and the distance from `y` to `z` is always less than or equal to the distance from `x` to `y`. In mathematical terms, for all `x`, `y` and `z`, we have \|dist(x, z) - dist(y, z)\| ≤ dist(x, y). More concisely: For any pseudometric space `(α, dist)`, the triangle inequality holds: `\|dist(x, z) - dist(y, z)\| ≤ dist(x, y)` for all `x, y, z` in `α`.
`Metric.mem_uniformity_dist` theorem Metric.mem_uniformity_dist : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set (α × α)}, s ∈ uniformity α ↔ ∃ ε > 0, ∀ {a b : α}, dist a b < ε → (a, b) ∈ s This theorem states that for any type `α` that has an instance of a PseudoMetricSpace and any set `s` of ordered pairs from `α`, the set `s` is an element of the uniformity of `α` if and only if there exists a positive real number `ε` such that for any two elements `a` and `b` of `α`, if the distance between `a` and `b` is less than `ε`, then the ordered pair `(a, b)` is an element of `s`. In other words, it describes the conditions under which a set of pairs of points in a pseudometric space can be considered uniformly close with respect to some positive real number. More concisely: A set of ordered pairs from a pseudometric space is an element of its uniformity if and only if it contains all ordered pairs of points with distance less than some positive real number.
`Metric.nhds_basis_closedBall` theorem Metric.nhds_basis_closedBall : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α}, (nhds x).HasBasis (fun ε => 0 < ε) (Metric.closedBall x) := by sorry This theorem states that for any point `x` in a space of type `α` that has a pseudometric space structure, the neighborhood filter at `x` has a basis consisting of closed balls around `x`. Specifically, the basis sets are those closed balls `Metric.closedBall x ε` such that `ε` is a positive real number. In mathematical terms, this means that any neighborhood of `x` can be represented as a union of such closed balls, providing a fundamental structure for the topology of the pseudometric space. More concisely: For any point in a pseudometric space, the neighborhood filter has a basis consisting of closed balls around that point with positive real radii.

LeanAide GPT-4 documentation

Module: Mathlib.Topology.MetricSpace.PseudoMetric

Metric.isBounded_iff

theorem Metric.isBounded_iff : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α}, Bornology.IsBounded s ↔ ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C

Metric.mem_nhds_iff

theorem Metric.mem_nhds_iff : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {s : Set α}, s ∈ nhds x ↔ ∃ ε > 0, Metric.ball x ε ⊆ s := by sorry

nhds_comap_dist

theorem nhds_comap_dist : ∀ {α : Type u} [inst : PseudoMetricSpace α] (a : α), Filter.comap (fun x => dist x a) (nhds 0) = nhds a

Metric.dist_mem_uniformity

theorem Metric.dist_mem_uniformity : ∀ {α : Type u} [inst : PseudoMetricSpace α] {ε : ℝ}, 0 < ε → {p | dist p.1 p.2 < ε} ∈ uniformity α

coe_nndist

theorem coe_nndist : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x y : α), ↑(nndist x y) = dist x y

Metric.isClosed_ball

theorem Metric.isClosed_ball : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε : ℝ}, IsClosed (Metric.closedBall x ε)

dist_le_range_sum_of_dist_le

theorem dist_le_range_sum_of_dist_le : ∀ {α : Type u} [inst : PseudoMetricSpace α] {f : ℕ → α} (n : ℕ) {d : ℕ → ℝ}, (∀ {k : ℕ}, k < n → dist (f k) (f (k + 1)) ≤ d k) → dist (f 0) (f n) ≤ (Finset.range n).sum fun i => d i

Dist.ext

theorem Dist.ext : ∀ {α : Type u_3} (x y : Dist α), dist = dist → x = y

dist_le_Ico_sum_dist

theorem dist_le_Ico_sum_dist : ∀ {α : Type u} [inst : PseudoMetricSpace α] (f : ℕ → α) {m n : ℕ}, m ≤ n → dist (f m) (f n) ≤ (Finset.Ico m n).sum fun i => dist (f i) (f (i + 1))

Mathlib.Topology.MetricSpace.PseudoMetric._auxLemma.19

theorem Mathlib.Topology.MetricSpace.PseudoMetric._auxLemma.19 : ∀ {α : Type u} [inst : LT α] {x y : α}, (x > y) = (y < x)

finite_cover_balls_of_compact

theorem finite_cover_balls_of_compact : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α}, IsCompact s → ∀ {e : ℝ}, 0 < e → ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ x ∈ t, Metric.ball x e

ball_pi

theorem ball_pi : ∀ {β : Type v} {π : β → Type u_3} [inst : Fintype β] [inst_1 : (b : β) → PseudoMetricSpace (π b)] (x : (b : β) → π b) {r : ℝ}, 0 < r → Metric.ball x r = Set.univ.pi fun b => Metric.ball (x b) r

Mathlib.Topology.MetricSpace.PseudoMetric._auxLemma.7

theorem Mathlib.Topology.MetricSpace.PseudoMetric._auxLemma.7 : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x y : α} {ε : ℝ}, (y ∈ Metric.ball x ε) = (dist y x < ε)

dist_le_range_sum_dist

theorem dist_le_range_sum_dist : ∀ {α : Type u} [inst : PseudoMetricSpace α] (f : ℕ → α) (n : ℕ), dist (f 0) (f n) ≤ (Finset.range n).sum fun i => dist (f i) (f (i + 1))

Metric.mem_ball_self

theorem Metric.mem_ball_self : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε : ℝ}, 0 < ε → x ∈ Metric.ball x ε

Metric.ball_mem_nhds

theorem Metric.ball_mem_nhds : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x : α) {ε : ℝ}, 0 < ε → Metric.ball x ε ∈ nhds x

dist_triangle

theorem dist_triangle : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x y z : α), dist x z ≤ dist x y + dist y z := by sorry

Metric.closure_ball_subset_closedBall

theorem Metric.closure_ball_subset_closedBall : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε : ℝ}, closure (Metric.ball x ε) ⊆ Metric.closedBall x ε := by sorry

Metric.emetric_closedBall_nnreal

theorem Metric.emetric_closedBall_nnreal : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε : NNReal}, EMetric.closedBall x ↑ε = Metric.closedBall x ↑ε

Metric.uniformity_basis_edist

theorem Metric.uniformity_basis_edist : ∀ {α : Type u} [inst : PseudoMetricSpace α], (uniformity α).HasBasis (fun ε => 0 < ε) fun ε => {p | edist p.1 p.2 < ε}

Real.dist_eq

theorem Real.dist_eq : ∀ (x y : ℝ), dist x y = |x - y|

Metric.mem_closure_iff

theorem Metric.mem_closure_iff : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} {a : α}, a ∈ closure s ↔ ∀ ε > 0, ∃ b ∈ s, dist a b < ε

dist_comm

theorem dist_comm : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x y : α), dist x y = dist y x

Metric.closedBall_zero'

theorem Metric.closedBall_zero' : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x : α), Metric.closedBall x 0 = closure {x}

Metric.mk_uniformity_basis

theorem Metric.mk_uniformity_basis : ∀ {α : Type u} [inst : PseudoMetricSpace α] {β : Type u_3} {p : β → Prop} {f : β → ℝ}, (∀ (i : β), p i → 0 < f i) → (∀ ⦃ε : ℝ⦄, 0 < ε → ∃ i, p i ∧ f i ≤ ε) → (uniformity α).HasBasis p fun i => {p | dist p.1 p.2 < f i}

nndist_triangle

theorem nndist_triangle : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x y z : α), nndist x z ≤ nndist x y + nndist y z

Metric.eventually_nhds_prod_iff

IsCompact.isSeparable

theorem IsCompact.isSeparable : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α}, IsCompact s → TopologicalSpace.IsSeparable s

Metric.sphere_subset_closedBall

theorem Metric.sphere_subset_closedBall : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε : ℝ}, Metric.sphere x ε ⊆ Metric.closedBall x ε

Mathlib.Topology.MetricSpace.PseudoMetric._auxLemma.47

theorem Mathlib.Topology.MetricSpace.PseudoMetric._auxLemma.47 : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x y : α}, (0 ≤ dist x y) = True

Metric.closedBall_eq_empty

theorem Metric.closedBall_eq_empty : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε : ℝ}, Metric.closedBall x ε = ∅ ↔ ε < 0

Metric.tendsto_nhds

theorem Metric.tendsto_nhds : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] {f : Filter β} {u : β → α} {a : α}, Filter.Tendsto u f (nhds a) ↔ ∀ ε > 0, ∀ᶠ (x : β) in f, dist (u x) a < ε

nndist_pi_def

theorem nndist_pi_def : ∀ {β : Type v} {π : β → Type u_3} [inst : Fintype β] [inst_1 : (b : β) → PseudoMetricSpace (π b)] (f g : (b : β) → π b), nndist f g = Finset.univ.sup fun b => nndist (f b) (g b)

Metric.ball_subset_closedBall

theorem Metric.ball_subset_closedBall : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε : ℝ}, Metric.ball x ε ⊆ Metric.closedBall x ε

dist_nonneg

theorem dist_nonneg : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x y : α}, 0 ≤ dist x y

Metric.totallyBounded_of_finite_discretization

theorem Metric.totallyBounded_of_finite_discretization : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α}, (∀ ε > 0, ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε) → TotallyBounded s

PseudoMetricSpace.ext

theorem PseudoMetricSpace.ext : ∀ {α : Type u_3} {m m' : PseudoMetricSpace α}, PseudoMetricSpace.toDist = PseudoMetricSpace.toDist → m = m' := by sorry

dist_triangle_left

theorem dist_triangle_left : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x y z : α), dist x y ≤ dist z x + dist z y

Metric.emetric_ball

theorem Metric.emetric_ball : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε : ℝ}, EMetric.ball x (ENNReal.ofReal ε) = Metric.ball x ε

Metric.tendsto_nhds_nhds

`Metric.isBounded_iff`

`Metric.mem_nhds_iff`

`nhds_comap_dist`

`Metric.dist_mem_uniformity`

`coe_nndist`

`Metric.isClosed_ball`

`dist_le_range_sum_of_dist_le`

`Dist.ext`

`dist_le_Ico_sum_dist`

`Mathlib.Topology.MetricSpace.PseudoMetric._auxLemma.19`

`finite_cover_balls_of_compact`

`ball_pi`

`Mathlib.Topology.MetricSpace.PseudoMetric._auxLemma.7`

`dist_le_range_sum_dist`

`Metric.mem_ball_self`

`Metric.ball_mem_nhds`

`dist_triangle`

`Metric.closure_ball_subset_closedBall`

`Metric.emetric_closedBall_nnreal`

`Metric.uniformity_basis_edist`

`Real.dist_eq`

`Metric.mem_closure_iff`

`dist_comm`

`Metric.closedBall_zero'`

`Metric.mk_uniformity_basis`

`nndist_triangle`

`Metric.eventually_nhds_prod_iff`

`IsCompact.isSeparable`

`Metric.sphere_subset_closedBall`

`Mathlib.Topology.MetricSpace.PseudoMetric._auxLemma.47`

`Metric.closedBall_eq_empty`

`Metric.tendsto_nhds`

`nndist_pi_def`

`Metric.ball_subset_closedBall`

`dist_nonneg`

`Metric.totallyBounded_of_finite_discretization`

`PseudoMetricSpace.ext`

`dist_triangle_left`

`Metric.emetric_ball`

`Metric.tendsto_nhds_nhds`

`Metric.uniformity_basis_dist_le`

`Metric.tendstoLocallyUniformly_iff`

`Metric.ball_subset_ball`

`totallyBounded_Icc`

`uniformContinuous_dist`

`Metric.closedBall_eq_sphere_of_nonpos`

`dist_pi_le_iff`

`Metric.forall_of_forall_mem_ball`

`Metric.secondCountable_of_almost_dense_set`

`Metric.mem_closedBall`

`Metric.isOpen_iff`

`Metric.eball_top_eq_univ`

`IsCompact.finite_cover_balls`

`edist_dist`

`continuous_dist`

`Metric.mem_sphere`

`Metric.uniformContinuous_iff`

`Metric.nhds_basis_ball`

`Metric.closedBall_subset_closedBall`

`dist_triangle_right`

`dist_pi_lt_iff`

`sphere_pi`

`Metric.controlled_of_uniformEmbedding`

`dist_pi_const`

`closedBall_pi'`

`Metric.emetric_closedBall`

`Metric.tendstoUniformly_iff`

`Metric.inseparable_iff`

`Metric.closedBall_mem_nhds`

`Metric.exists_lt_mem_ball_of_mem_ball`

`Metric.tendsto_atTop'`

`Mathlib.Topology.MetricSpace.PseudoMetric._auxLemma.65`

`Metric.tendstoUniformlyOn_iff`

`Metric.ball_eq_empty`