Mathlib.Topology.MetricSpace.Infsep._auxLemma.5
theorem Mathlib.Topology.MetricSpace.Infsep._auxLemma.5 : ∀ {b a : Prop}, (∃ (_ : a), b) = (a ∧ b)
This theorem, under the `Mathlib.Topology.MetricSpace.Infsep._auxLemma.5` namespace, states that for any two propositions `a` and `b`, the existence of `b` under the assumption that `a` is true, is equivalent to `a` and `b` both being true. In other words, "there exists `a` such that `b` is true" is logically equivalent to "`a` and `b` are both true".
More concisely: The theorem asserts that for any propositions `a` and `b` in Lean's type theory, `∃ (x : Prop), a × b → a ∧ b` holds.
|
Set.le_einfsep
theorem Set.le_einfsep :
∀ {α : Type u_1} [inst : EDist α] {s : Set α} {d : ENNReal},
(∀ x ∈ s, ∀ y ∈ s, x ≠ y → d ≤ edist x y) → d ≤ s.einfsep
This theorem states that for any type `α` equipped with an "extended" distance function, any set `s` of elements of type `α`, and any extended nonnegative real number `d`, if for every pair of distinct elements `x` and `y` in `s` the distance between `x` and `y` is at least `d`, then `d` is less than or equal to the "extended infimum separation" of the set `s`. The "extended infimum separation" of a set is defined as the infimum of the distances between distinct pairs of elements in the set.
More concisely: Given a type `α` with an extended distance function, if `s` is a set of distinct elements of `α` such that the distance between any two elements is at least `d`, then `d` is less than or equal to the infimum of the distances between distinct pairs in `s`.
|
Mathlib.Topology.MetricSpace.Infsep._auxLemma.21
theorem Mathlib.Topology.MetricSpace.Infsep._auxLemma.21 :
∀ {α : Type u} {x : α × α} {s : Set α}, (x ∈ s.offDiag) = (x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2)
This theorem, `Mathlib.Topology.MetricSpace.Infsep._auxLemma.21`, states that for any type `α`, any pair `x` of type `α × α`, and any set `s` of type `Set α`, the pair `x` belongs to the off-diagonal of `s` if and only if the first element of `x` belongs to `s`, the second element of `x` belongs to `s` and the first element of `x` is not equal to the second element of `x`. In other words, a pair `(a, b)` is in the off-diagonal of a set if and only if both `a` and `b` are in the set and `a` is not equal to `b`.
More concisely: For any set `s` and type `α`, a pair `(a, b)` in `α × α` lies off-diagonal in `s` if and only if both `a` and `b` are in `s` and `a ≠ b`.
|
Set.einfsep_pos_of_finite
theorem Set.einfsep_pos_of_finite :
∀ {α : Type u_1} [inst : EMetricSpace α] {s : Set α} [inst_1 : Finite ↑s], 0 < s.einfsep
The theorem `Set.einfsep_pos_of_finite` states that for any set `s` of a given type `α`, where `α` is an extended metric space and the set `s` is finite, the "extended infimum separation" of that set `s` is strictly greater than 0. The "extended infimum separation", denoted by `Set.einfsep s`, is defined as the infimum of the extended distances between all distinct pairs of elements from the set. In simpler terms, the theorem claims that in a finite set within an extended metric space, the smallest distance between any two distinct points is always a positive number.
More concisely: In an extended metric space, the extended infimum separation of any finite set is positive.
|
Set.le_einfsep_iff
theorem Set.le_einfsep_iff :
∀ {α : Type u_1} [inst : EDist α] {s : Set α} {d : ENNReal},
d ≤ s.einfsep ↔ ∀ x ∈ s, ∀ y ∈ s, x ≠ y → d ≤ edist x y
This theorem states that for any type `α` with an extended distance (`EDist`) function, any set `s` of elements of type `α`, and any extended nonnegative real number `d`, `d` is less than or equal to the extended infimum separation of the set `s` if and only if for all distinct elements `x` and `y` in the set `s`, `d` is less than or equal to the extended distance between `x` and `y`. In other words, `d` is bounded below by the minimum extended distance between any two distinct elements of the set `s`.
More concisely: For any set `s` of elements in a type `α` with an extended distance function, and any extended nonnegative real number `d`, `d` is less than or equal to the extended infimum separation of `s` if and only if it is less than or equal to the minimum extended distance between any distinct elements of `s`.
|
Mathlib.Topology.MetricSpace.Infsep._auxLemma.22
theorem Mathlib.Topology.MetricSpace.Infsep._auxLemma.22 :
∀ {α : Type u_1} {β : Type u_2} {p : α × β → Prop}, (∀ (x : α × β), p x) = ∀ (a : α) (b : β), p (a, b)
This theorem, named `Mathlib.Topology.MetricSpace.Infsep._auxLemma.22`, states that for any types `α` and `β` and a property `p` defined on the Cartesian product of `α` and `β`, stating that the property `p` holds for all pairs `(a, b)` in the product space is equivalent to saying that for every `x` in the Cartesian product `α × β`, the property `p` holds. In other words, the two formulations of universality (one in terms of individual elements `x` from the product space, and the other in terms of pairs `(a, b)`) are logically equivalent.
More concisely: The theorem `Mathlib.Topology.MetricSpace.Infsep._auxLemma.22` in Lean 4 asserts that for any types `α` and `β` and a property `p` on `α × β`, the statements "for all `(a, b)` in `α × β`, `p(a, b)` holds" and "for all `x` in `α × β`, `p(x)` holds" are logically equivalent.
|
Set.einfsep_le_edist_of_mem
theorem Set.einfsep_le_edist_of_mem :
∀ {α : Type u_1} [inst : EDist α] {s : Set α} {x : α}, x ∈ s → ∀ {y : α}, y ∈ s → x ≠ y → s.einfsep ≤ edist x y
The theorem `Set.einfsep_le_edist_of_mem` states that for any type `α` equipped with an extended distance (or `edist`) function, and for any set `s` of elements of type `α`, if `x` and `y` are distinct elements of `s`, then the extended infimum separation of `s` is less than or equal to the extended distance between `x` and `y`. This essentially says that the smallest possible separation in a set is always less than or equal to the distance between any two distinct elements in the set.
More concisely: For any set equipped with an extended distance function, the extended infimum separation of distinct elements is less than or equal to their extended distance.
|
Mathlib.Topology.MetricSpace.Infsep._auxLemma.25
theorem Mathlib.Topology.MetricSpace.Infsep._auxLemma.25 :
∀ {α : Type u_1} {s : Set α} [inst : Fintype ↑s] {a : α}, (a ∈ s.toFinset) = (a ∈ s)
This theorem states that for any type `α`, any set `s` of elements of type `α` with a `Fintype` instance, and any element `a` of type `α`, the membership of `a` in the finset derived from `s` using the `Set.toFinset` function is equivalent to the membership of `a` in the set `s` itself. This means if `a` is an element of the set `s`, then it will be an element of the finset created from `s`, and vice versa.
More concisely: For any type `α` with a `Fintype` instance, and any set `s` of type `α` and element `a` of type `α`, `a` belongs to the finset `Set.toFinset s` if and only if it belongs to the set `s` itself.
|
Mathlib.Topology.MetricSpace.Infsep._auxLemma.4
theorem Mathlib.Topology.MetricSpace.Infsep._auxLemma.4 :
∀ {α : Type u_1} {ι : Sort u_5} [inst : CompleteLinearOrder α] {a : α} {f : ι → α}, (iInf f < a) = ∃ i, f i < a
The theorem, `Mathlib.Topology.MetricSpace.Infsep._auxLemma.4`, states that for any type `α`, which is a complete linear order, and any function `f` from an arbitrary index set `ι` to `α`, and for any element `a` of type `α`, the statement that the indexed infimum of `f` is less than `a` is equivalent to the existence of an index `i` such that `f(i)` is less than `a`. In other words, the infimum of the range of `f` being less than `a` means there exists some element in the range of `f` which is less than `a`.
More concisely: For any complete linear order `α` and function `f` from an index set `ι` to `α`, the infimum of `f` is less than `a` if and only if there exists an index `i` such that `f(i)` is less than `a`.
|
Mathlib.Topology.MetricSpace.Infsep._auxLemma.1
theorem Mathlib.Topology.MetricSpace.Infsep._auxLemma.1 :
∀ {α : Type u_1} {ι : Sort u_5} [inst : CompleteLattice α] {f : ι → α} {a : α}, (a ≤ iInf f) = ∀ (i : ι), a ≤ f i
This theorem, `Mathlib.Topology.MetricSpace.Infsep._auxLemma.1`, states that for any type `α` that forms a `CompleteLattice`, any function `f` from an arbitrary type `ι` to `α`, and any element `a` of type `α`, the inequality `a ≤ iInf f` holds if and only if `a` is less than or equal to `f i` for all `i` of type `ι`. Here, `iInf` is the indexed infimum function which takes a function from `ι` to `α` and returns the greatest lower bound of the set of all values of the function.
More concisely: For any complete lattice α and function f from type ι to α, element a belongs to the indexed infimum iInf(f) if and only if a is less than or equal to f(i) for all i of type ι.
|
Set.Subsingleton.einfsep
theorem Set.Subsingleton.einfsep : ∀ {α : Type u_1} [inst : EDist α] {s : Set α}, s.Subsingleton → s.einfsep = ⊤ := by
sorry
The theorem `Set.Subsingleton.einfsep` states that for any type `α` equipped with an extended distance function (`EDist α`), and for any set `s` of this type, if `s` is a subsingleton (that is, if it has at most one element), then the extended infimum separation of `s` is equal to the extended non-negative real number infinity (`⊤`). The extended infimum separation of a set is the greatest lower bound of the distance between distinct elements of the set. In case of a subsingleton set, since there are either zero or one elements, the distance between distinct elements is undefined and thus considered as infinity.
More concisely: For any type `α` with an extended distance function and any subsingleton set `s` of `α`, the extended infimum separation of `s` equals the infinity symbol `⊤`.
|
Mathlib.Topology.MetricSpace.Infsep._auxLemma.19
theorem Mathlib.Topology.MetricSpace.Infsep._auxLemma.19 :
∀ {α : Type u_3} {p : Prop} {q : α → Prop}, (p → ∀ (x : α), q x) = ∀ (x : α), p → q x
This theorem, `Mathlib.Topology.MetricSpace.Infsep._auxLemma.19`, states that for any type 'α', any proposition 'p', and any predicate 'q' on 'α', the statement that "if 'p' holds then 'q' holds for all 'x' in 'α'" is equivalent to the statement "for all 'x' in 'α', if 'p' holds then 'q' holds". In other words, it's a proposition about the interchangeability of the universal quantifier and the implication in a certain context.
More concisely: For any type 'α', proposition 'p' on 'α', and predicate 'q' on 'α', the statements "forall x in α, if p(x) then q(x)" and "if p then forall x in α, q(x)" are equivalent.
|
Mathlib.Topology.MetricSpace.Infsep._auxLemma.23
theorem Mathlib.Topology.MetricSpace.Infsep._auxLemma.23 : ∀ {a b c : Prop}, (a ∧ b → c) = (a → b → c)
This theorem, `Mathlib.Topology.MetricSpace.Infsep._auxLemma.23`, states that for any three propositions `a`, `b`, and `c`, the statement "`a` and `b` imply `c`" is logically equivalent to the statement "`a` implies that `b` implies `c`". In other words, if having both propositions `a` and `b` leads to proposition `c`, then it is the same as saying if `a` is true, then `b` leading to `c` is also true. This is a fundamental theorem in logic, reflecting the associativity of logical implication.
More concisely: The proposition "`a` implies `b` implies `c`" is logically equivalent to "`a` and `b` imply `c`" for any propositions `a`, `b`, and `c`.
|
Set.Nontrivial.le_infsep_iff
theorem Set.Nontrivial.le_infsep_iff :
∀ {α : Type u_1} [inst : PseudoMetricSpace α] {s : Set α} {d : ℝ},
s.Nontrivial → (d ≤ s.infsep ↔ ∀ x ∈ s, ∀ y ∈ s, x ≠ y → d ≤ dist x y)
This theorem states that for any type `α` that forms a pseudometric space, for any nontrivial set `s` of `α`, and for any real number `d`, the condition `d` being less than or equal to the infimum separation of `s` is equivalent to the condition that for any two distinct elements `x` and `y` in `s`, the distance between `x` and `y` is greater than or equal to `d`. Here, a set is nontrivial if it has at least two distinct elements, and the infimum separation of a set is the greatest lower bound of the distances between all pairs of distinct elements in the set.
More concisely: For any pseudometric space `α` and nontrivial set `s` in `α`, the infimum separation of `s` equals the smallest distance `d` such that for all distinct `x, y` in `s`, the distance between `x` and `y` is greater than or equal to `d`.
|
Mathlib.Topology.MetricSpace.Infsep._auxLemma.13
theorem Mathlib.Topology.MetricSpace.Infsep._auxLemma.13 :
∀ {α : Type u_1} [inst : EDist α] {s : Set α} {d : ENNReal},
(d ≤ s.einfsep) = ∀ x ∈ s, ∀ y ∈ s, x ≠ y → d ≤ edist x y
This theorem is about extended nonnegative real valued distances (edist) in a set `s` of some type `α` equipped with an extended distance function (`EDist`). The theorem states that for any extended nonnegative real number `d` and any set `s`, `d` is less than or equal to the extended infimum separation of `s` if and only if for all distinct elements `x` and `y` in `s`, `d` is less than or equal to the edist between `x` and `y`. The extended infimum separation of a set with respect to a distance function is the greatest lower bound of the separations among all pairs of distinct elements in the set, where separation `edist x y` is the extended distance between elements `x` and `y`.
More concisely: For a set `s` in type `α` with an extended distance function `EDist`, a non-negative extended real number `d` is less than or equal to the extended infimum separation of `s` if and only if `d` is less than or equal to the extended distance between every distinct pair of elements in `s`.
|
Set.Subsingleton.infsep_zero
theorem Set.Subsingleton.infsep_zero : ∀ {α : Type u_1} [inst : EDist α] {s : Set α}, s.Subsingleton → s.infsep = 0
This theorem states that for any set `s` of a certain type `α` that has an extended distance (edist) function defined, if `s` is a subsingleton set (meaning it contains at most one element), then the infimum separation of the set `s` is zero. The infimum separation of a set, as per the `Set.infsep` definition, is the real equivalent of the least separation between any two points in the set. Therefore, intuitively, if a set consists of at most one point, there are no two points to calculate the separation between, so the infimum separation is zero.
More concisely: For any set `s` of type `α` with an extended distance function, if `s` is a subsingleton, then its infimum separation is 0.
|
Set.Nontrivial.einfsep_ne_top
theorem Set.Nontrivial.einfsep_ne_top :
∀ {α : Type u_1} [inst : PseudoMetricSpace α] {s : Set α}, s.Nontrivial → s.einfsep ≠ ⊤
The theorem `Set.Nontrivial.einfsep_ne_top` states that for any nontrivial set `s` in a pseudo metric space `α`, the extended infimum separation of the set `s` is not equal to the positive infinity. Here, a set is said to be nontrivial if it contains at least two distinct elements and the extended infimum separation of a set `s` is defined as the greatest lower bound of the extended distances between distinct pairs of elements in `s`.
More concisely: In a pseudo metric space, the extended infimum separation of a nontrivial set is strictly less than positive infinity.
|