IsMetricSeparated.finite_iUnion_left_iff
theorem IsMetricSeparated.finite_iUnion_left_iff :
∀ {X : Type u_1} [inst : EMetricSpace X] {ι : Type u_2} {I : Set ι},
I.Finite →
∀ {s : ι → Set X} {t : Set X}, IsMetricSeparated (⋃ i ∈ I, s i) t ↔ ∀ i ∈ I, IsMetricSeparated (s i) t
This theorem states that for any type `X` that has an extended metric space structure, a set `I` of any type `ι`, and a function `s` mapping `ι` to a set of `X`, and a set `t` of type `X`, if `I` is finite, then the union of the sets `s i` for each `i` in `I` is metric-separated from `t` if and only if each set `s i` is metric-separated from `t`. In other words, a union of sets is metric-separated from another set `t` if and only if each individual set in the union is metric-separated from `t`, given that the index set over which the union is taken is finite. Here, two sets are considered metric-separated if there exists a positive constant that is a lower bound for the distance between any pair of elements where one element is from the first set and the other is from the second set.
More concisely: For any finite index set `I`, a union of metric-separated sets `{s i : X | i ∈ I}` is metric-separated from a set `t` if and only if each `s i` is metric-separated from `t` in an extended metric space.
|
IsMetricSeparated.finset_iUnion_left
theorem IsMetricSeparated.finset_iUnion_left :
∀ {X : Type u_1} [inst : EMetricSpace X] {ι : Type u_2} {I : Finset ι} {s : ι → Set X} {t : Set X},
(∀ i ∈ I, IsMetricSeparated (s i) t) → IsMetricSeparated (⋃ i ∈ I, s i) t
This theorem, also known as the reverse direction of `IsMetricSeparated.finset_iUnion_left_iff`, states that in any extended metric space `X`, if for a given indexed family of sets `{s i}` and another set `t`, each set `s i` is metric separated from `t` (meaning that the distance between any element of `s i` and `t` is no less than a certain positive number), then the union of these sets `{s i}` (taken over all `i` in some finite set `I`) is also metric separated from `t`.
More concisely: In an extended metric space, if each element of an indexed family of sets is metrically separated from a given set, then their union is also metrically separated from that set.
|
IsMetricSeparated.symm
theorem IsMetricSeparated.symm :
∀ {X : Type u_1} [inst : EMetricSpace X] {s t : Set X}, IsMetricSeparated s t → IsMetricSeparated t s
This theorem states that if two sets in an extended metric space are metric separated, this property is symmetric. In other words, if for every pair of points with the first point from the first set and the second point from the second set there exists a non-zero lower bound for their distance, then the same holds true if the roles of the two sets are swapped. This means that the concept of metric separation between two sets is independent from the order in which we consider the sets.
More concisely: If sets A and B are metric separated in an extended metric space, then B and A are also metric separated.
|
IsMetricSeparated.finset_iUnion_right
theorem IsMetricSeparated.finset_iUnion_right :
∀ {X : Type u_1} [inst : EMetricSpace X] {ι : Type u_2} {I : Finset ι} {s : Set X} {t : ι → Set X},
(∀ i ∈ I, IsMetricSeparated s (t i)) → IsMetricSeparated s (⋃ i ∈ I, t i)
This theorem, being an alias for the reverse direction of `IsMetricSeparated.finset_iUnion_right_iff`, states that for any type `X` with an extended metric space structure, a set `s` of type `X`, a finset `I` of another type `ι`, and a function `t` that maps elements of type `ι` to sets of type `X`, if for every element `i` in `I`, the set `s` is metric separated from the set `t i`, then `s` is also metric separated from the union of all `t i` for `i` in `I`.
In simpler terms, if a particular set is metric separated from each of several other sets, then it is also metric separated from the union of those other sets. Here, being "metric separated" means that there is a positive lower bound on the distance between any point in one set and any point in the other.
More concisely: If a set is metrically separated from each set in a family, then it is metrically separated from their union.
|
IsMetricSeparated.finite_iUnion_left
theorem IsMetricSeparated.finite_iUnion_left :
∀ {X : Type u_1} [inst : EMetricSpace X] {ι : Type u_2} {I : Set ι},
I.Finite →
∀ {s : ι → Set X} {t : Set X}, (∀ i ∈ I, IsMetricSeparated (s i) t) → IsMetricSeparated (⋃ i ∈ I, s i) t
This theorem states that if we have a finite set `I` of indices and for each index `i` in `I`, the set `s i` is metric separated from another set `t` in an extended metric space `X`, then the union of these `s i` sets is also metric separated from `t`. In other words, if each of a collection of finite sets is at least a certain positive distance from a given set, then the union of that collection of sets is also at least that distance from the given set.
More concisely: If `{si : i ∈ I}` is a family of metric subsets of a metric space `(X, d)` such that for all `i ∈ I`, we have `d(x, si) ≥ r` for some `r > 0` and all `x ∈ t`, then `d(x, ⋃ i ∈ I si) ≥ r` for all `x ∈ X`.
|