interior_closedBall
theorem interior_closedBall :
∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (x : E) {r : ℝ},
r ≠ 0 → interior (Metric.closedBall x r) = Metric.ball x r
This theorem, `interior_closedBall`, states that for any type `E` which is a semi-normed additive commutative group and also a normed space over the real numbers, and for any element `x` of type `E` and real number `r` not equal to zero, the interior of the closed ball centered at `x` with radius `r` is equal to the open ball centered at `x` with radius `r`. Here, the "interior" of a set is defined as the largest open subset of that set. The "closed ball" around a point `x` with radius `r` consists of all points `y` such that the distance from `y` to `x` is less than or equal to `r`. The "open ball" around a point `x` with radius `r` consists of all points `y` such that the distance from `y` to `x` is strictly less than `r`.
More concisely: For any semi-normed additive commutative group and normed space E over the real numbers, the interior of the closed ball with center x and radius r equals the open ball with center x and radius r for all non-zero r.
|
closure_ball
theorem closure_ball :
∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (x : E) {r : ℝ},
r ≠ 0 → closure (Metric.ball x r) = Metric.closedBall x r
The theorem `closure_ball` states that for any given seminormed additive commutative group `E` equipped with a normed space over the real numbers, any point `x` in `E`, and any nonzero real number `r`, the closure of the open ball centered at `x` with radius `r` is equal to the closed ball with the same center and radius. In other words, the smallest closed set which contains the open ball (all points within a distance `r` from `x`, but not including the boundary) is the closed ball itself (all points within a distance `r` from `x`, including the boundary).
More concisely: The closure of an open ball in a normed space equals the corresponding closed ball.
|