EMetric.eventually_nhds_zero_forall_closedBall_subset
theorem EMetric.eventually_nhds_zero_forall_closedBall_subset :
∀ {ι : Type u_1} {X : Type u_2} [inst : EMetricSpace X] {K U : ι → Set X},
(∀ (i : ι), IsClosed (K i)) →
(∀ (i : ι), IsOpen (U i)) →
(∀ (i : ι), K i ⊆ U i) →
LocallyFinite K →
∀ (x : X),
∀ᶠ (p : ENNReal × X) in nhds 0 ×ˢ nhds x, ∀ (i : ι), p.2 ∈ K i → EMetric.closedBall p.2 p.1 ⊆ U i
The theorem `EMetric.eventually_nhds_zero_forall_closedBall_subset` states the following in an extended metric space $X$: Given a locally finite family of closed sets $K : \iota \rightarrow Set\ X$ and a family of open sets $U : \iota \rightarrow Set\ X$, where each $K_i$ is a subset of $U_i$ for all $i$. Then for any point $x$ in the space $X$, there exists a sufficiently small non-negative extended real number $r$ and a point $y$ sufficiently close to $x$, such that for all indices $i$, if $y$ is an element of $K_i$, then the closed ball around $y$ with radius $r$ is contained within $U_i$. This theorem essentially states that within these conditions, we can always find an open set $U_i$ that fully contains the closed ball around $y$.
More concisely: Given a locally finite family of closed sets $K : \iota \rightarrow X$ and a family of open sets $U : \iota \rightarrow X$ with $K_i \subseteq U_i$ for all $i$, for each point $x$ in $X$, there exists a sufficiently small $r \ge 0$ and a point $y$ close to $x$ such that $B(y,r) \subseteq U_i$ for all $i$ where $y \in K_i$.
|
EMetric.exists_continuous_eNNReal_forall_closedBall_subset
theorem EMetric.exists_continuous_eNNReal_forall_closedBall_subset :
∀ {ι : Type u_1} {X : Type u_2} [inst : EMetricSpace X] {K U : ι → Set X},
(∀ (i : ι), IsClosed (K i)) →
(∀ (i : ι), IsOpen (U i)) →
(∀ (i : ι), K i ⊆ U i) →
LocallyFinite K → ∃ δ, (∀ (x : X), 0 < δ x) ∧ ∀ (i : ι), ∀ x ∈ K i, EMetric.closedBall x (δ x) ⊆ U i
This theorem states that given an extended metric space `X` and a locally finite family `K` of closed sets, along with another family `U` of open sets such that each set in `K` is a subset of the corresponding set in `U`, there exists a positive, continuous function `δ` that maps from `X` to the set of nonnegative extended real numbers. For any point `x` in any set `K[i]`, the closed ball centered at `x` with radius `δ(x)` is a subset of `U[i]`. Here, a closed ball is defined as the set of all points whose extended distance from the center is less than or equal to the radius.
More concisely: Given an extended metric space `X` and a locally finite family `K` of closed sets with each `K[i]` being a subset of the corresponding open set `U[i]`, there exists a continuous, positive function `δ: X → ℝ↑+` such that for all `x ∈ K[i]`, the closed ball `B(x, δ(x))` is contained in `U[i]`.
|
EMetric.exists_continuous_real_forall_closedBall_subset
theorem EMetric.exists_continuous_real_forall_closedBall_subset :
∀ {ι : Type u_1} {X : Type u_2} [inst : EMetricSpace X] {K U : ι → Set X},
(∀ (i : ι), IsClosed (K i)) →
(∀ (i : ι), IsOpen (U i)) →
(∀ (i : ι), K i ⊆ U i) →
LocallyFinite K →
∃ δ, (∀ (x : X), 0 < δ x) ∧ ∀ (i : ι), ∀ x ∈ K i, EMetric.closedBall x (ENNReal.ofReal (δ x)) ⊆ U i
The theorem `EMetric.exists_continuous_real_forall_closedBall_subset` states that given an extended metric space `X`, a locally finite family `K` of closed sets, and another family `U` of open sets such that each set in `K` is a subset of the corresponding set in `U`, there exists a positive continuous function `δ` from `X` to the real numbers such that for any `i` and any `x` in `K i`, the closed ball centered at `x` with radius equal to the nonnegative part of `δ(x)` is a subset of `U i`. In other words, for each point in every closed set, we can find a ball around that point which fits entirely inside the corresponding open set.
More concisely: Given an extended metric space, a locally finite family of closed sets, and another family of open sets with each closed set a subset of the corresponding open set, there exists a continuous positive function such that for each closed set and its point, the closed ball around the point with radius equal to the function value is contained in the open set.
|
Metric.exists_continuous_real_forall_closedBall_subset
theorem Metric.exists_continuous_real_forall_closedBall_subset :
∀ {ι : Type u_1} {X : Type u_2} [inst : MetricSpace X] {K U : ι → Set X},
(∀ (i : ι), IsClosed (K i)) →
(∀ (i : ι), IsOpen (U i)) →
(∀ (i : ι), K i ⊆ U i) →
LocallyFinite K → ∃ δ, (∀ (x : X), 0 < δ x) ∧ ∀ (i : ι), ∀ x ∈ K i, Metric.closedBall x (δ x) ⊆ U i
The theorem `Metric.exists_continuous_real_forall_closedBall_subset` states that given a metric space `X` and a locally finite family `K` of closed sets, alongside a family `U` of open sets such that each set `K i` is contained within the corresponding set `U i`, there exists a positive continuous function `δ` mapped from `X` to the set of real numbers. This function has the property that, for any `i` and any `x` in `K i`, the closed ball in the metric space centered at `x` with radius `δ x` is contained within `U i`.
More concisely: Given a metric space with a locally finite family of closed sets and an open cover such that each closed set is contained in its open set, there exists a continuous positive function whose closed balls about each point include that point and are contained within the corresponding open set.
|