absorbent_nhds_zero
theorem absorbent_nhds_zero :
∀ {𝕜 : Type u_1} {E : Type u_3} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] {A : Set E}
[inst_3 : TopologicalSpace E] [inst_4 : ContinuousSMul 𝕜 E], A ∈ nhds 0 → Absorbent 𝕜 A
This theorem states that for any type `𝕜` which is a normed field and any type `E` which is an additive commutative group and a module over `𝕜`, if `A` is a set in `E` and `E` is a topological space with a continuous scalar multiplication, then any neighborhood of the origin in `E` (indicating that `A` is in the neighborhood filter at `0`) is an absorbent set. In other words, every neighborhood of the origin has the property that for any element `x` in `E`, there is a set in `𝕜` that, when every element of this set is used to scale `x`, the result is within `A`.
More concisely: For any normed field `𝕜`, any additive commutative group and `𝕜`-module `E` with continuous scalar multiplication, if `A` is a neighborhood of the origin in `E` and `x` is any element in `E`, then there exists a set `S` in `𝕜` such that for all `r` in `S`, `rx` is in `A`.
|
Balanced.smul_mem
theorem Balanced.smul_mem :
∀ {𝕜 : Type u_1} {E : Type u_3} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] {s : Set E},
Balanced 𝕜 s → ∀ ⦃a : 𝕜⦄, ‖a‖ ≤ 1 → ∀ ⦃x : E⦄, x ∈ s → a • x ∈ s
The theorem `Balanced.smul_mem` states that for any seminormed ring `𝕜` and any type `E` with a scalar multiplication operation by `𝕜`, if a set `s` of elements of type `E` is balanced, then for any element `a` of `𝕜` with norm at most `1` and any element `x` of `s`, the scalar multiplication of `a` and `x` is also an element of `s`. In simpler terms, if a set is balanced, then scaling any member of the set by a factor whose size is at most 1 yields another member of the set.
More concisely: For any seminormed ring `𝕜` and type `E` with scalar multiplication, if `s` is a balanced set of `E` and `a` is an element of `𝕜` with norm at most 1, then `ax` is in `s` for all `x` in `s`.
|
Balanced.interior
theorem Balanced.interior :
∀ {𝕜 : Type u_1} {E : Type u_3} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] {A : Set E}
[inst_3 : TopologicalSpace E] [inst_4 : ContinuousSMul 𝕜 E],
Balanced 𝕜 A → 0 ∈ interior A → Balanced 𝕜 (interior A)
This theorem states that for any type `𝕜` which is a normed field, any type `E` which is a topological space, an additive commutative group, and a module over `𝕜`, and any set `A` of type `E`, if `A` is a balanced set and the origin is contained in the interior of `A`, then the interior of `A` is also a balanced set.
Here, a set is balanced if, for every element `a` of norm at most `1`, the scalar multiplication of `a` and the set is a subset of the original set. The interior of a set is the largest open subset of that set.
More concisely: If `A` is an open, balanced subset of a normed vector space `E` over a normed field `𝕜` with origin in `A`, then `A` is a balanced set.
|
Absorbs.of_norm
theorem Absorbs.of_norm :
∀ {𝕜 : Type u_1} {E : Type u_3} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] {A B : Set E},
(∃ r, ∀ (c : 𝕜), r ≤ ‖c‖ → B ⊆ c • A) → Absorbs 𝕜 A B
This theorem, referred to as an alias in reverse direction of `absorbs_iff_norm`, states that for any types `𝕜` and `E`, where `𝕜` is a semi-normed ring and `E` is a scalar multiplication of `𝕜`, and for any sets `A` and `B` of type `E`, if there exists some real number `r` such that for all `c` in `𝕜`, `r` is less than or equal to the norm of `c` and `B` is a subset of `c` scaled by `A`, then `A` absorbs `B`. In other words, no matter how much you scale `A` by `c`, `B` will always be contained within it, provided `c` has a norm greater than or equal to `r`.
More concisely: If `𝕜` is a semi-normed ring, `E` is its scalar multiplication, `r` is a real number, `A` and `B` are sets of `E`, and for all `c` in `𝕜`, `r` is less than or equal to the norm of `c` implies `B` is a subset of `c` scaled by `A`, then `A` absorbs `B`.
|
Absorbs.exists_pos
theorem Absorbs.exists_pos :
∀ {𝕜 : Type u_1} {E : Type u_3} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] {A B : Set E},
Absorbs 𝕜 A B → ∃ r > 0, ∀ (c : 𝕜), r ≤ ‖c‖ → B ⊆ c • A
The theorem `Absorbs.exists_pos` states that given any two sets `A` and `B` of elements of a type `E`, under the conditions that `𝕜` is a seminormed ring and `E` has scalar multiplication by `𝕜`, if `A` absorbs `B`, then there exists a positive number `r` such that for all elements `c` of `𝕜`, if `r` is less than or equal to the seminorm of `c`, then `B` is a subset of the scalar multiple of `A` by `c`. Essentially, the theorem guarantees the existence of a positive lower bound that scales `A` to include `B` under the seminormed ring multiplication operation.
Here, "absorption" is defined in terms of a concept from topology called "bornology", where `A` absorbs `B` if `B` is contained in all scalings of `A` except those by a bounded set of elements.
More concisely: Given a seminormed ring `𝕜` and sets `A` and `B` in the module `E` over `𝕜`, if `A` absorbs `B` in the bornology sense, then there exists a positive number `r` such that `B` is contained in the scalar multiples of `A` by elements of `𝕜` with seminorm less than or equal to `r`.
|
Balanced.absorbs_self
theorem Balanced.absorbs_self :
∀ {𝕜 : Type u_1} {E : Type u_3} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] {A : Set E},
Balanced 𝕜 A → Absorbs 𝕜 A A
The theorem `Balanced.absorbs_self` states that for any normed field `𝕜` and additive commutative group `E` with a module structure over `𝕜`, and for any set `A` of elements in `E`, if `A` is balanced, then `A` absorbs itself. In other words, if every scalar multiple of `A` by elements of `𝕜` with norm at most `1` is contained within `A`, then `A` is contained within all scalings of itself by all elements of `𝕜` except those in a bounded set.
More concisely: If `A` is a balanced subset of a normed vector space `(𝕜, E)` over a normed field `𝕜`, then for all `x` in `𝕜` with norm less than or equal to 1, `xA ⊆ A`.
|
Balanced.smul_mono
theorem Balanced.smul_mono :
∀ {𝕜 : Type u_1} {𝕝 : Type u_2} {E : Type u_3} [inst : NormedField 𝕜] [inst_1 : NormedRing 𝕝]
[inst_2 : NormedSpace 𝕜 𝕝] [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] [inst_5 : SMulWithZero 𝕝 E]
[inst_6 : IsScalarTower 𝕜 𝕝 E] {s : Set E}, Balanced 𝕝 s → ∀ {a : 𝕝} {b : 𝕜}, ‖a‖ ≤ ‖b‖ → a • s ⊆ b • s
The theorem `Balanced.smul_mono` states that for any types `𝕜`, `𝕝` and `E`, given instances of `NormedField 𝕜`, `NormedRing 𝕝`, `NormedSpace 𝕜 𝕝`, `AddCommGroup E`, `Module 𝕜 E`, `SMulWithZero 𝕝 E`, and `IsScalarTower 𝕜 𝕝 E`, if a set `s` of type `E` is balanced with respect to `𝕝`, then for any scalar `a` of type `𝕝` and scalar `b` of type `𝕜`, if the norm of `a` is less than or equal to the norm of `b`, the scalar multiplication of `a` with `s` is a subset of the scalar multiplication of `b` with `s`. In simpler terms, the theorem states that scalar multiplication of a balanced set is a monotonically increasing operation with respect to the norm of the scalars.
More concisely: If `s` is a balanced set in a Normed Space `E` over a Normed Field `𝕜` with respect to a Normed Ring `𝕝`, then for any `a` in `𝕝` with norm less than or equal to `b` in `𝕜`, the scalar multiplication of `a` with `s` is a subset of the scalar multiplication of `b` with `s`.
|
balanced_zero_union_interior
theorem balanced_zero_union_interior :
∀ {𝕜 : Type u_1} {E : Type u_3} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] {A : Set E}
[inst_3 : TopologicalSpace E] [inst_4 : ContinuousSMul 𝕜 E], Balanced 𝕜 A → Balanced 𝕜 (0 ∪ interior A)
This theorem states that for any set `A` of a type `E` in a particular topological space and module structure over a normed field `𝕜`, if `A` is a balanced set (meaning that scaling `A` by any element `a` of `𝕜` with a norm not greater than 1 results in a subset of `A`), then the set resulting from the union of `A` with the set containing only the zero element and the interior of `A` (the largest open subset of `A`), is also a balanced set. This holds under the condition that the scalar multiplication operation is continuous in this topological space.
More concisely: Given a balanced set `A` in a topological space with a normed field scalar multiplication that is continuous, the set `A ∪ {0} ∪ int(A)` is also balanced.
|