Balanced.balancedHull_subset_of_subset
theorem Balanced.balancedHull_subset_of_subset :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] {s t : Set E},
Balanced 𝕜 t → s ⊆ t → balancedHull 𝕜 s ⊆ t
The theorem `Balanced.balancedHull_subset_of_subset` states that for any type `𝕜` which forms a semi-normed ring and any type `E` on which `𝕜` acts scalarily (`SMul 𝕜 E`), if `s` and `t` are sets of elements of type `E` and `t` is a balanced set, then if `s` is a subset of `t`, the balanced hull of `s` (i.e., the smallest balanced set containing `s`) is also a subset of `t`. This essentially means that the balanced hull of `s` is the minimal balanced set containing `s` in the sense that it is contained in any other balanced set that contains `s`.
More concisely: If `𝕜` is a semi-normed ring and `E` is a type on which `𝕜` acts scalarly, and `t` is a balanced set in `E` and `s` is a subset of `t`, then the balanced hull of `s` is also a subset of `t`.
|
Balanced.subset_balancedCore_of_subset
theorem Balanced.subset_balancedCore_of_subset :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] {s t : Set E},
Balanced 𝕜 s → s ⊆ t → s ⊆ balancedCore 𝕜 t
The theorem `Balanced.subset_balancedCore_of_subset` states that for any types `𝕜` and `E`, given a seminormed ring structure on `𝕜` and a scalar multiplication structure on `E`, if `s` and `t` are two sets of elements in `E`, and `s` is a balanced set, then if `s` is a subset of `t`, `s` is also a subset of the balanced core of `t`. In other words, the balanced core of a set `t` is maximal in the sense that it contains any other balanced subset `s` of `t`. Here, a set is balanced if when we scale its elements by a scalar `a` with norm at most `1`, the resulting scaled set remains contained within the original set.
More concisely: If `s` is a balanced subset of `E` and `s` is a subset of `t`, then `s` is a subset of the balanced core of `t`.
|
balancedCore_mem_nhds_zero
theorem balancedCore_mem_nhds_zero :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
[inst_3 : TopologicalSpace E] [inst_4 : ContinuousSMul 𝕜 E] {U : Set E}, U ∈ nhds 0 → balancedCore 𝕜 U ∈ nhds 0
This theorem states that for any non-trivial normed field `𝕜` and an additive commutative group `E` over which `𝕜` is a module, if `U` is a set in `E` that belongs to the neighborhood of zero in the topological space of `E`, then the largest balanced subset of `U` also belongs to the neighborhood of zero. Here, a balanced set is one that is stable under scalar multiplication. The theorem assumes that the action of `𝕜` on `E` is continuous.
More concisely: If `U` is a neighborhood of zero in a normed vector space `(𝕜, E)` over a non-trivial normed field `𝕜`, where the `𝕜`-module action on `E` is continuous, then the largest balanced subset of `U` is also a neighborhood of zero.
|
balancedCore_balanced
theorem balancedCore_balanced :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] (s : Set E),
Balanced 𝕜 (balancedCore 𝕜 s)
The theorem `balancedCore_balanced` states that for any given seminormed ring `𝕜` and scalar multiplication (`SMul`) on type `E`, and for any set `s` of type `E`, the largest balanced subset within `s` (denoted as `balancedCore 𝕜 s`) is balanced. In other words, if `a` is an element in ring `𝕜` with the property that its norm is at most `1`, then the scalar multiplication of `a` and the `balancedCore` is contained within the `balancedCore` itself.
More concisely: For any seminormed ring `𝕜` and subset `s` of its type `E`, the balanced subset `balancedCore 𝕜 s` is closed under scalar multiplication by elements in `𝕜` with norm at most 1.
|
balancedCore_subset
theorem balancedCore_subset :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] (s : Set E), balancedCore 𝕜 s ⊆ s
The theorem `balancedCore_subset` states that for any type `𝕜` with a structure of seminormed ring and any type `E` with a structure of scalar multiplication by `𝕜`, for any set `s` of elements of `E`, the balanced core of `s` is always a subset of `s`. In other words, all elements of the balanced core of a set are also elements of the original set.
More concisely: For any seminormed ring `𝕜` and any scalar multiplication module `E` over `𝕜`, the balanced core of any subset `s` of `E` is contained in `s`.
|