ConvexBody.iInter_smul_eq_self
theorem ConvexBody.iInter_smul_eq_self :
∀ {V : Type u_1} [inst : SeminormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [inst_2 : T2Space V] {u : ℕ → NNReal}
(K : ConvexBody V), 0 ∈ K → Filter.Tendsto u Filter.atTop (nhds 0) → ⋂ n, (1 + ↑(u n)) • ↑K = ↑K
This theorem states that given a convex body `K` in a normed space over the reals that contains the origin, and a sequence of nonnegative real numbers `u` that tends to `0`, the intersection of all the dilations of `K` by factors of `(1 + u n)` equals `K` itself. Here, a dilation of `K` by a factor `r` means each point in `K` is moved `r` times further away from the origin. The requirement that `u` tends to `0` ensures that as `n` increases, the amount of dilation decreases, effectively squeezing back to the original set `K`.
More concisely: Given a convex body `K` in a normed space over the reals containing the origin, and a sequence `u_n` of real numbers converging to `0`, the intersection of all sets obtained by dilating `K` by factors `(1 + u_n)` is equal to `K`.
|
ConvexBody.hausdorffEdist_ne_top
theorem ConvexBody.hausdorffEdist_ne_top :
∀ {V : Type u_1} [inst : SeminormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] {K L : ConvexBody V},
EMetric.hausdorffEdist ↑K ↑L ≠ ⊤
The theorem `ConvexBody.hausdorffEdist_ne_top` states that for any type `V` which is a seminormed additive commutative group and a real normed space, the Hausdorff edistance between the underlying sets of any two convex bodies `K` and `L` in `V` is never equal to positive infinity. Here, the Hausdorff edistance between two sets is defined as the smallest `r` such that each set is contained in the `r`-neighborhood of the other one.
More concisely: The Hausdorff distance between any two convex bodies in a seminormed additive commutative group and real normed space is finite.
|
ConvexBody.convex
theorem ConvexBody.convex :
∀ {V : Type u_1} [inst : TopologicalSpace V] [inst_1 : AddCommGroup V] [inst_2 : Module ℝ V] (K : ConvexBody V),
Convex ℝ ↑K
The theorem `ConvexBody.convex` states that for any convex body `K` in a topological space `V` (which is also an additive commutative group and a real number `ℝ` module), the convex body `K` is a convex set in `V` with respect to `ℝ`. In other words, for any two points within this convex body, the entire line segment that joins these two points also lies within the convex body.
More concisely: For any convex body K in a topological vector space V with real scalars, every line segment contained in K is also a subset of K.
|
ConvexBody.nonempty
theorem ConvexBody.nonempty :
∀ {V : Type u_1} [inst : TopologicalSpace V] [inst_1 : AddCommGroup V] [inst_2 : Module ℝ V] (K : ConvexBody V),
(↑K).Nonempty
This theorem states that for any type `V` which is equipped with a topological space structure, an additive commutative group structure, and a real number module structure, every convex body `K` in `V` is non-empty. In other words, there exists at least one element in `V` that is a member of the convex body `K`. This theorem works regardless of the specifics of the type `V` as long as the appropriate structures are defined.
More concisely: Every convex body in a topological vector space is non-empty.
|
ConvexBody.zero_mem_of_symmetric
theorem ConvexBody.zero_mem_of_symmetric :
∀ {V : Type u_1} [inst : TopologicalSpace V] [inst_1 : AddCommGroup V] [inst_2 : Module ℝ V] (K : ConvexBody V),
(∀ x ∈ K, -x ∈ K) → 0 ∈ K
This theorem states that for any convex body `K` in a real vector space `V`, if `K` is symmetric (i.e., for every point `x` in `K`, its negation `-x` is also in `K`), then the origin `0` is contained in `K`. Here, `V` is a topological space, an additive commutative group, and a module over the real numbers.
More concisely: If `K` is a convex and symmetric subset of a real vector space `V`, then the origin `0` is an element of `K`.
|
ConvexBody.isCompact
theorem ConvexBody.isCompact :
∀ {V : Type u_1} [inst : TopologicalSpace V] [inst_1 : AddCommGroup V] [inst_2 : Module ℝ V] (K : ConvexBody V),
IsCompact ↑K
The theorem `ConvexBody.isCompact` states that for any given convex body `K` in a real vector space `V` (where `V` is a topological space and also an additive commutative group), the set corresponding to `K` is compact. Here, a set is compact if for every nontrivial filter `f` that contains the set, there exists an element `a` in the set such that every set in `f` meets every neighborhood of `a`. This is essentially saying that the convex body `K` has the property that every collection of closed sets with the finite intersection property has a non-empty intersection.
More concisely: A convex body in a real vector space is compact if and only if every filter containing it has an element with the property that every neighborhood of that element intersects every set in the filter.
|