LeanAide documentation

LeanAide GPT-4 documentation

Module: Mathlib.Analysis.LocallyConvex.Bounded

`Bornology.IsVonNBounded.of_add_right` theorem Bornology.IsVonNBounded.of_add_right : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] [inst_4 : ContinuousSMul 𝕜 E] [inst_5 : ContinuousAdd E] {s t : Set E}, Bornology.IsVonNBounded 𝕜 (s + t) → s.Nonempty → Bornology.IsVonNBounded 𝕜 t The theorem `Bornology.IsVonNBounded.of_add_right` states that for any types `𝕜` and `E` with `𝕜` being a normed field, `E` being an additive commutative group, and a module over `𝕜`, if we have a continuous scalar multiplication and addition on `E`, then for any two sets `s` and `t` of type `E`, if the set `s + t` is von Neumann bounded and the set `s` is not empty, then the set `t` is also von Neumann bounded. In other words, if `s` is a nonempty set and `s + t` is a von Neumann bounded set, then `t` must also be a von Neumann bounded set. Here, `s + t` is the set of all elements that can be written as the sum of an element from `s` and an element from `t`, and a set being von Neumann bounded means that every neighborhood of 0 absorbs that set. More concisely: If `𝕜` is a normed field, `E` is an additive commutative group and a `𝕜`-module, `s` is a nonempty set in `E`, and `s + t` is von Neumann bounded, then `t` is also von Neumann bounded.
`Bornology.IsVonNBounded.neg` theorem Bornology.IsVonNBounded.neg : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : SeminormedRing 𝕜] [inst_1 : AddGroup E] [inst_2 : TopologicalSpace E] [inst_3 : TopologicalAddGroup E] [inst_4 : DistribMulAction 𝕜 E] {s : Set E}, Bornology.IsVonNBounded 𝕜 s → Bornology.IsVonNBounded 𝕜 (-s) The theorem `Bornology.IsVonNBounded.neg` states that for any seminormed ring `𝕜` and any set `s` in a topological vector space `E` over `𝕜` that forms a topological group under addition, if `s` is von Neumann bounded (meaning that every neighborhood of 0 absorbs `s`), then the negation of `s` (i.e., the set of all additive inverses of elements of `s`) is also von Neumann bounded. This theorem essentially asserts the symmetry of von Neumann boundedness under negation in a topological vector space. More concisely: In a topological vector space over a seminormed ring, if a set absorbs every neighborhood of zero, then the negation of the set also absorbs every neighborhood of zero.
`NormedSpace.vonNBornology_eq` theorem NormedSpace.vonNBornology_eq : ∀ (𝕜 : Type u_1) (E : Type u_3) [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E], Bornology.vonNBornology 𝕜 E = PseudoMetricSpace.toBornology The theorem `NormedSpace.vonNBornology_eq` states that in a normed space, the von Neumann bornology (a structure that encodes boundedness properties) is equivalent to the metric bornology (the set of all bounded sets in a pseudometric space). In other words, these two ways of defining boundedness in a normed space - one via the von Neumann bounded sets and the other via the metric-based pseudometric space - result in the same bornology. More concisely: In a normed space, the von Neumann bornology and the metric bornology are equal.
`Bornology.isVonNBounded_singleton` theorem Bornology.isVonNBounded_singleton : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] [inst_4 : ContinuousSMul 𝕜 E] (x : E), Bornology.IsVonNBounded 𝕜 {x} The theorem `Bornology.isVonNBounded_singleton` states that for any singleton set, consisting of a single element `x` from a space `E`, the set is von Neumann bounded in the context of a normed field `𝕜`. In more technical terms, for any given neighborhood `V` of zero in `E`, there exists a scalar from `𝕜` such that scalar multiplication of `V` can cover the element `x`. The type `E` has a structure of a topological space, a module over the normed field `𝕜`, and the scalar multiplication from `𝕜` to `E` is continuous. More concisely: For any singleton set in a topological module over a normed field endowed with a continuous scalar multiplication, there exists a scalar such that scalar multiplication covers the set.
`Bornology.IsVonNBounded.image` theorem Bornology.IsVonNBounded.image : ∀ {E : Type u_3} {F : Type u_5} {𝕜₁ : Type u_7} {𝕜₂ : Type u_8} [inst : NormedDivisionRing 𝕜₁] [inst_1 : NormedDivisionRing 𝕜₂] [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜₁ E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜₂ F] [inst_6 : TopologicalSpace E] [inst_7 : TopologicalSpace F] {σ : 𝕜₁ →+* 𝕜₂} [inst_8 : RingHomSurjective σ] [inst_9 : RingHomIsometric σ] {s : Set E}, Bornology.IsVonNBounded 𝕜₁ s → ∀ (f : E →SL[σ] F), Bornology.IsVonNBounded 𝕜₂ (⇑f '' s) The theorem `Bornology.IsVonNBounded.image` states that, given a set `s` of elements of some type `E` that is von Neumann bounded in a normed division ring `𝕜₁`, then the image of `s` under any continuous linear map `f` into some type `F` in another normed division ring `𝕜₂` is also von Neumann bounded in `𝕜₂`. Here, a set being von Neumann bounded means that every neighborhood of 0 in the space "absorbs" the set, meaning that there is a scalar such that multiplying every element of the set by the scalar results in elements all inside the neighborhood. The theorem ensures that this property is preserved under continuous linear transformation. More concisely: Given a von Neumann bounded set in a normed division ring and a continuous linear map between two normed division rings, the image of the set is also von Neumann bounded.
`Bornology.IsVonNBounded.subset` theorem Bornology.IsVonNBounded.subset : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] [inst_2 : Zero E] [inst_3 : TopologicalSpace E] {s₁ s₂ : Set E}, s₁ ⊆ s₂ → Bornology.IsVonNBounded 𝕜 s₂ → Bornology.IsVonNBounded 𝕜 s₁ The theorem `Bornology.IsVonNBounded.subset` states that, given any seminormed ring `𝕜` and any set `E` that is a smul (scalar multiplication), a zero, and a topological space, if we have two subsets `s₁` and `s₂` of `E`, and `s₁` is a subset of `s₂`, then if `s₂` is von Neumann bounded (meaning that every neighborhood of zero absorbs `s₂`), `s₁` is also von Neumann bounded. In other words, the subset of a bounded set is also bounded. More concisely: If `s₁` is a subset of von Neumann bounded `s₂` in a seminormed ring `𝕜` and `E` with `E` being a smul, a zero, and a topological space, then `s₁` is von Neumann bounded.
`Bornology.IsVonNBounded.of_topologicalSpace_le` theorem Bornology.IsVonNBounded.of_topologicalSpace_le : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] {t t' : TopologicalSpace E}, t ≤ t' → ∀ {s : Set E}, Bornology.IsVonNBounded 𝕜 s → Bornology.IsVonNBounded 𝕜 s This theorem asserts that if a topology `t'` is coarser than (or equal to) another topology `t`, then any set `s` that is von Neumann bounded with respect to `t` will also be von Neumann bounded with respect to `t'`. In other words, the property of a set being von Neumann bounded is preserved under passing to a coarser topology. Here, von Neumann boundedness means that for every neighborhood of the zero element, there is a positive scalar such that multiplying the set `s` by this scalar gets the entire set `s` inside the neighborhood. More concisely: If topology `t'` is coarser than or equal to topology `t`, then any `s` von Neumann bounded in `t` is also von Neumann bounded in `t'`.
`NormedSpace.isVonNBounded_closedBall` theorem NormedSpace.isVonNBounded_closedBall : ∀ (𝕜 : Type u_1) (E : Type u_3) [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] (r : ℝ), Bornology.IsVonNBounded 𝕜 (Metric.closedBall 0 r) The theorem `NormedSpace.isVonNBounded_closedBall` states that for any nontrivially normed field `𝕜`, seminormed additive commutative group `E`, normed space over `𝕜` and `E`, and a real number `r`, the closed ball in the metric space centered at zero with radius `r` is von Neumann bounded. In other words, every neighborhood of zero absorbs this closed ball in the given normed space. More concisely: In a normed space over a nontrivially normed field, the closed ball centered at the zero point is von Neumann bounded.
`Bornology.IsVonNBounded.add` theorem Bornology.IsVonNBounded.add : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : SeminormedRing 𝕜] [inst_1 : AddZeroClass E] [inst_2 : TopologicalSpace E] [inst_3 : ContinuousAdd E] [inst_4 : DistribSMul 𝕜 E] {s t : Set E}, Bornology.IsVonNBounded 𝕜 s → Bornology.IsVonNBounded 𝕜 t → Bornology.IsVonNBounded 𝕜 (s + t) The theorem `Bornology.IsVonNBounded.add` states that for any two sets `s` and `t` in a topological space `E` over a seminormed ring `𝕜`, if both `s` and `t` are von Neumann bounded (meaning every neighbourhood of 0 absorbs them), then the sum of `s` and `t` (defined as `s + t`) is also von Neumann bounded. Here, `E` has the additional structures of an additive zero class and a continuous addition operation, and the scalar multiplication by `𝕜` is distributive over the addition in `E`. More concisely: If two sets in a topological space over a seminormed ring are von Neumann bounded, then their sum is also von Neumann bounded.
`NormedSpace.isVonNBounded_ball` theorem NormedSpace.isVonNBounded_ball : ∀ (𝕜 : Type u_1) (E : Type u_3) [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] (r : ℝ), Bornology.IsVonNBounded 𝕜 (Metric.ball 0 r) The theorem `NormedSpace.isVonNBounded_ball` states that for any nontrivially normed field `𝕜`, any seminormed additive commutative group `E`, and any given normed space over `𝕜` and `E`, the metric ball centered at zero with radius `r` (which is the set of all points whose distance from zero is less than `r`) is von Neumann bounded. In other words, every neighborhood of zero in the topological space `E` can absorb the metric ball. This absorption suggests that any element of the metric ball can be scaled by a factor from the field `𝕜` such that it lies within any given neighborhood of zero. More concisely: For any nontrivially normed field `𝕜`, any seminormed additive commutative group `E` made into a normed space over `𝕜`, and any `r` in `𝕜` such that the metric ball in `E` centered at zero with radius `r` is nonempty, it holds that this ball is von Neumann bounded, meaning for any neighborhood of zero `U` in `E`, there exists `s` in `𝕜` such that the ball with radius `sr` is contained in `U`.
`Filter.HasBasis.isVonNBounded_basis_iff` theorem Filter.HasBasis.isVonNBounded_basis_iff : ∀ {𝕜 : Type u_1} {E : Type u_3} {ι : Type u_6} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] [inst_2 : Zero E] [inst_3 : TopologicalSpace E] {q : ι → Prop} {s : ι → Set E} {A : Set E}, (nhds 0).HasBasis q s → (Bornology.IsVonNBounded 𝕜 A ↔ ∀ (i : ι), q i → Absorbs 𝕜 (s i) A) The theorem `Filter.HasBasis.isVonNBounded_basis_iff` states that for any sets of types `𝕜`, `E`, and `ι`, given that `𝕜` is a seminormed ring, `E` is a set that can be scaled by `𝕜` and has a zero element and a topological structure, and given a predicate `q` on `ι` and a function `s` from `ι` to a set of `E`, and another set `A` of `E`, if the neighborhood filter of 0 has a basis characterized by `q` and `s`, then `A` is von Neumann bounded in `𝕜` if and only if for every `i` in `ι` that satisfies `q`, the set `A` gets absorbed by all except a cobounded set of scalings of `s i` by `𝕜`. Here, a set is von Neumann bounded if every neighborhood of 0 absorbs it, and a set `s` absorbs another set `t` if `t` is contained in all scalings of `s` by all but a bounded set of elements. More concisely: For a seminormed ring `𝕜`, set `E` with a topology, predicate `q` on `ι`, function `s` from `ι` to `E`, and set `A` of `E`, `A` is von Neumann bounded if and only if for every `i` in `ι` satisfying `q`, `A` is contained in all but a cobounded set of scalings of `s i` by `𝕜`.
`NormedSpace.isVonNBounded_iff` theorem NormedSpace.isVonNBounded_iff : ∀ (𝕜 : Type u_1) (E : Type u_3) [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] (s : Set E), Bornology.IsVonNBounded 𝕜 s ↔ Bornology.IsBounded s This theorem, `NormedSpace.isVonNBounded_iff`, states that for any types `𝕜` and `E`, where `𝕜` is a nontrivially-normed field and `E` is a seminormed additive commutative group that forms a normed space over `𝕜`, a set `s` of type `E` is von Neumann bounded with respect to `𝕜` if and only if it is bounded relative to the ambient bornology on `E`. Here, von Neumann boundedness means that every neighborhood of 0 absorbs the set `s`, and boundedness in the sense of bornology means that the set's complement is cobounded. More concisely: A set in a normed space is von Neumann bounded if and only if it is bounded in the ambient bornology.
`Bornology.isVonNBounded_empty` theorem Bornology.isVonNBounded_empty : ∀ (𝕜 : Type u_1) (E : Type u_3) [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] [inst_2 : Zero E] [inst_3 : TopologicalSpace E], Bornology.IsVonNBounded 𝕜 ∅ This theorem states that for any type `𝕜` which is a semi-normed ring, and any type `E` which is a zero element, a topological space, and allows scalar multiplication by `𝕜`, the empty set is von Neumann bounded. In other words, for all neighborhoods `V` of zero in the vector space `E`, `V` absorbs the empty set. This means that there exists a scalar in `𝕜` such that scaling `V` by this scalar contains the empty set, which is trivially true. More concisely: For any semi-normed ring `𝕜` and topological vector space `E` over `𝕜` with zero element, the empty set is von Neumann bounded, i.e., there exists a scalar `r` in `𝕜` such that `{x ∈ E \| r * x = ∅}` (the scalar multiplication of `r` with the empty set).
`Bornology.isVonNBounded_covers` theorem Bornology.isVonNBounded_covers : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] [inst_4 : ContinuousSMul 𝕜 E], (setOf (Bornology.IsVonNBounded 𝕜)).sUnion = Set.univ The theorem `Bornology.isVonNBounded_covers` states that for any normed field `𝕜`, any additive commutative group `E`, any `𝕜`-module structure on `E`, any topological space structure on `E`, and any continuous scalar multiplication from `𝕜` to `E`, the union of all von Neumann-bounded sets is the universal set (i.e., the entire space). In other words, every point in the space can be covered by von Neumann-bounded sets. Here, a set is said to be von Neumann-bounded if every neighborhood of the origin absorbs the set. More concisely: In a normed field with a continuous scalar multiplication on a topological vector space, every point is contained in the union of von Neumann-bounded sets.
`Bornology.IsVonNBounded.union` theorem Bornology.IsVonNBounded.union : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] [inst_2 : Zero E] [inst_3 : TopologicalSpace E] {s₁ s₂ : Set E}, Bornology.IsVonNBounded 𝕜 s₁ → Bornology.IsVonNBounded 𝕜 s₂ → Bornology.IsVonNBounded 𝕜 (s₁ ∪ s₂) This theorem states that for any two sets `s₁` and `s₂` of a certain type `E`, if both these sets are von Neumann bounded with respect to a seminormed ring `𝕜`, then their union is also von Neumann bounded with respect to the same seminormed ring `𝕜`. In this context, a set is said to be von Neumann bounded if every neighborhood of 0 absorbs the set. A neighborhood of 0 absorbs a set if there is a scalar such that multiplying every member of the set by this scalar results in points that all lie within the neighborhood. More concisely: If sets `s₁` and `s₂` in seminormed ring `𝕜` are both von Neumann bounded, then their union is also von Neumann bounded.
`Bornology.isVonNBounded_iff_smul_tendsto_zero` theorem Bornology.isVonNBounded_iff_smul_tendsto_zero : ∀ {E : Type u_3} {ι : Type u_6} {𝕝 : Type u_7} [inst : NontriviallyNormedField 𝕝] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕝 E] [inst_3 : TopologicalSpace E] [inst_4 : ContinuousSMul 𝕝 E] {ε : ι → 𝕝} {l : Filter ι} [inst_5 : l.NeBot], Filter.Tendsto ε l (nhdsWithin 0 {0}ᶜ) → ∀ {S : Set E}, Bornology.IsVonNBounded 𝕝 S ↔ ∀ (x : ι → E), (∀ (n : ι), x n ∈ S) → Filter.Tendsto (ε • x) l (nhds 0) This theorem states that for any nontrivially normed field `𝕝` and for any set `S` of elements in a topological space `E` that is a module over `𝕝`, `S` is Von Neumann bounded (meaning every neighborhood of 0 absorbs `S`) if and only if for any function `x` from an indexing type `ι` to `E` such that every value of `x` is in `S`, the function `ε • x` (where `ε` is any function from `ι` to `𝕝` that tends to non-zero values close to 0) tends to 0. This holds for any filter `l` on `ι` which is not bottom (i.e., it does not contain all sets). In simpler terms, a set is bounded in a module over a field if and only if, for any sequence in that set, multiplying the sequence by a sequence of scalars that tends to 0 produces a sequence that tends to 0. Particularly, if `ι` is the natural numbers, this theorem shows that we can characterize bounded sets using convergent sequences. More concisely: A set in a topological module over a nontrivially normed field is Von Neumann bounded if and only if for any sequence in the set indexed by an arbitrary non-bottom filter, the product of the sequence with any sequence of scalars tending to zero also tends to zero.