Absorbs.iUnion
theorem Absorbs.iUnion :
∀ {M : Type u_1} {α : Type u_2} [inst : Bornology M] [inst_1 : SMul M α] {s : Set α} {ι : Sort u_3}
[inst_2 : Finite ι] {t : ι → Set α}, (∀ (i : ι), Absorbs M s (t i)) → Absorbs M s (⋃ i, t i)
The theorem `Absorbs.iUnion` states that for any types `M` and `α`, where `M` is equipped with a Bornology structure and `α` is equipped with a scalar multiplication by `M`, and for any set `s` of type `α` and any finite indexed collection `{t : ι → Set α}` of sets of type `α`, if every individual set `t i` is absorbed by `s` under the scalar multiplication, then the union of all these sets `(⋃ i, t i)` is also absorbed by `s`. "Absorbed" here means that each `t i` or `(⋃ i, t i)` is contained in all scalings of `s` by all but a bounded set of elements in `M`.
More concisely: For any type `α` with scalar multiplication by a Bornology-structured type `M`, if every set in a finite collection is absorbed by a set `s` in `α`, then their union is also absorbed by `s`.
|
Set.Finite.absorbs_biUnion
theorem Set.Finite.absorbs_biUnion :
∀ {M : Type u_1} {α : Type u_2} [inst : Bornology M] [inst_1 : SMul M α] {s : Set α} {ι : Type u_3} {t : ι → Set α}
{I : Set ι}, I.Finite → (Absorbs M s (⋃ i ∈ I, t i) ↔ ∀ i ∈ I, Absorbs M s (t i))
This theorem, `Set.Finite.absorbs_biUnion`, states that for any type `M` with a Bornology structure, a type `α` with a scalar multiplication by `M`, a set `s` of type `α`, an indexing type `ι`, a function `t` from `ι` to sets of `α`, and a finite set `I` of `ι`, the set `s` absorbs the union of the sets `t i` for `i` in `I` if and only if `s` absorbs each of the sets `t i` for each `i` in `I`. Here, a set `s` is said to absorb another set `t` if `t` is contained in all scalings of `s` by all but a bounded set of elements from `M`.
More concisely: For a type with a Bornology structure `M`, a scalar multiplication `α × M → α`, a set `s ⊆ α`, a family `t` of sets `ι → α`, and a finite set `I ⊆ ι`, `s` absorbs the union of `t i` for `i` in `I` if and only if it absorbs each `t i` for all `i` in `I`.
|
Set.Finite.absorbs_sInter
theorem Set.Finite.absorbs_sInter :
∀ {G₀ : Type u_1} {α : Type u_2} [inst : GroupWithZero G₀] [inst_1 : Bornology G₀] [inst_2 : MulAction G₀ α]
{t : Set α} {S : Set (Set α)}, S.Finite → (Absorbs G₀ S.sInter t ↔ ∀ s ∈ S, Absorbs G₀ s t)
The theorem `Set.Finite.absorbs_sInter` states that for any types `G₀` and `α`, where `G₀` is a group with zero and has a bornology, and `α` is a set on which `G₀` acts multiplicatively, given a set `t` of type `α` and a set `S` of sets of type `α`, if `S` is finite, then `t` is absorbed by the intersection over `S` (denoted as `⋂₀ S`) if and only if `t` is absorbed by every set `s` in `S`.
In this context, a set `s` absorbs another set `t` if `t` is contained in all scalings of `s` by all but a bounded set of elements of `G₀`.
More concisely: For a group with zero and bornology `G₀` acting multiplicatively on set `α`, a set `t` is absorbed by the intersection of finite sets `S` if and only if it is absorbed by each set `s` in `S`.
|
Absorbs.biUnion
theorem Absorbs.biUnion :
∀ {M : Type u_1} {α : Type u_2} [inst : Bornology M] [inst_1 : SMul M α] {s : Set α} {ι : Type u_3} {t : ι → Set α}
{I : Set ι}, I.Finite → (∀ i ∈ I, Absorbs M s (t i)) → Absorbs M s (⋃ i ∈ I, t i)
The theorem `Absorbs.biUnion` states that for any types `M` and `α` with a bornology on `M` and scalar multiplication on `α`, given a set `s` of type `α`, an index set `I` of type `ι`, and a family of sets `t` indexed by `ι`, if `I` is finite and each set `t(i)` for `i` in `I` is absorbed by `s`, then the union of all `t(i)` for `i` in `I` is also absorbed by `s`. Absorption here means that except for a bounded set of elements in `M`, every element from the absorbed set can be obtained by scaling an element of the absorbing set.
More concisely: If `I` is a finite index set and each `t(i)` is absorbed by `s` in a bornology on `M` with scalar multiplication on `α`, then the union of all `t(i)` is absorbed by `s`.
|
Absorbs.sInter
theorem Absorbs.sInter :
∀ {G₀ : Type u_1} {α : Type u_2} [inst : GroupWithZero G₀] [inst_1 : Bornology G₀] [inst_2 : MulAction G₀ α]
{t : Set α} {S : Set (Set α)}, S.Finite → (∀ s ∈ S, Absorbs G₀ s t) → Absorbs G₀ S.sInter t
The theorem `Absorbs.sInter` establishes that for a type `G₀` equipped with a zero element and a group structure, a type `α` which `G₀` acts on via multiplication, a set `t` of type `α`, and a set `S` of sets of type `α` which is finite, if every set `s` in `S` absorbs `t` in the `G₀` context, then the intersection of all sets in `S` also absorbs `t`. In this context, a set `s` absorbs another set `t` if `t` is contained in all scalings of `s` by all but a bounded set of elements of `G₀`.
More concisely: If a finite set `S` of sets of an `α` that is acted upon by a group `G₀` with a zero element, absorbs a set `t` in the sense that `t` is contained in all but a bounded number of scalings of each set in `S`, then the intersection of all sets in `S` absorbs `t`.
|
Absorbs.biInter
theorem Absorbs.biInter :
∀ {G₀ : Type u_1} {α : Type u_2} [inst : GroupWithZero G₀] [inst_1 : Bornology G₀] [inst_2 : MulAction G₀ α]
{t : Set α} {ι : Type u_3} {I : Set ι},
I.Finite → ∀ {s : ι → Set α}, (∀ i ∈ I, Absorbs G₀ (s i) t) → Absorbs G₀ (⋂ i ∈ I, s i) t
This theorem, referred to as an alias of the reverse direction of `Set.Finite.absorbs_biInter`, states that given types `G₀` and `α` with a `GroupWithZero` structure and a `MulAction` structure on `G₀` and `α` respectively, along with a `Bornology` on `G₀`, a set `t` of type `α`, a type `ι`, and a set `I` of type `ι`, if `I` is finite and for every `i` in `I`, the set `s i` absorbs `t`, then the intersection of the sets `s i` over all `i` in `I` also absorbs `t`.
In other words, if every set `s i` absorbs `t` and the index set `I` is finite, then `t` is also absorbed by the intersection of all these sets `s i`. Here, absorption is defined as `t` being contained in all possible scalings of the set `s i` by all but a bounded set of elements in `G₀`.
More concisely: Given a finite index set `I`, a type `α` with `GroupWithZero` and `MulAction` structures, a `Bornology` on a type `G₀` with `GroupWithZero` structure, a set `t` of type `α`, and for each `i` in `I`, a set `s i` absorbing `t`, then the intersection of the `s i` absorbs `t`.
|
Absorbs.biUnion_finset
theorem Absorbs.biUnion_finset :
∀ {M : Type u_1} {α : Type u_2} [inst : Bornology M] [inst_1 : SMul M α] {s : Set α} {ι : Type u_3} {t : ι → Set α}
{I : Finset ι}, (∀ i ∈ I, Absorbs M s (t i)) → Absorbs M s (⋃ i ∈ I, t i)
The theorem `Absorbs.biUnion_finset` states that for any types `M` and `α`, where `M` has a Bornology structure and `α` is equipped with a scalar multiplication by `M`, and for any set `s` of type `α`, index set type `ι`, and a family of sets `t` indexed by `ι`, and for any finite set `I` of indices, if `s` absorbs each `t i` for all `i` in `I` (meaning each `t i` is contained in all but a bounded set of scalings of `s`), then `s` absorbs the union of the `t i` for all `i` in `I`. In simpler terms, if a set `s` absorbs each of a collection of sets, then it also absorbs their union.
More concisely: If a set `s` absorbs every set `t_i` in a finite family, then it absorbs their union.
|
absorbs_iUnion_finset
theorem absorbs_iUnion_finset :
∀ {M : Type u_1} {α : Type u_2} [inst : Bornology M] [inst_1 : SMul M α] {s : Set α} {ι : Type u_3} {t : ι → Set α}
{I : Finset ι}, Absorbs M s (⋃ i ∈ I, t i) ↔ ∀ i ∈ I, Absorbs M s (t i)
The theorem `absorbs_iUnion_finset` states that for any types `M` and `α`, given a bornology on `M` and a scalar multiplication on `α`, for any set `s` of type `α`, any type `ι`, and a function `t` mapping `ι` to a set of `α`, and for any finite set `I` of `ι`, a set `s` absorbs the union over the set `I` of the sets `t i` (where `i` is an element in `I`) if and only if `s` absorbs each of the sets `t i` for all `i` in `I`. Here, a set `s` absorbing another set `t` means that `t` is contained in all scalings of `s` by all but a bounded set of elements from `M`.
More concisely: For any bornology on a type M, scalar multiplication on a type α, and sets s of α, i : ι, and I a finite set of i, s absorbs the union of the sets ti if and only if it absorbs each ti. (Here, absorption means that each ti is contained in all but a bounded set of scalings of s by elements from M.)
|
Absorbs.iInter
theorem Absorbs.iInter :
∀ {G₀ : Type u_1} {α : Type u_2} [inst : GroupWithZero G₀] [inst_1 : Bornology G₀] [inst_2 : MulAction G₀ α]
{t : Set α} {ι : Sort u_3} [inst_3 : Finite ι] {s : ι → Set α},
(∀ (i : ι), Absorbs G₀ (s i) t) → Absorbs G₀ (⋂ i, s i) t
This theorem, named `Absorbs.iInter`, states that given a group with zero `G₀`, a set `t` in some type `α`, and a finite collection of sets `s` indexed by `ι`, if for every index `i`, the set `s i` absorbs the set `t`, then the intersection of all sets `s i` also absorbs `t`. Here "absorbs" means that `t` is contained in all scalings of the set by all but a bounded set of elements from `G₀` according to our Bornology on `G₀`.
More concisely: If each set in a finite collection absorbs a given set, then their intersection also absorbs it.
|
Absorbs.add
theorem Absorbs.add :
∀ {M : Type u_1} {E : Type u_2} [inst : Bornology M] {s₁ s₂ t₁ t₂ : Set E} [inst_1 : AddZeroClass E]
[inst_2 : DistribSMul M E], Absorbs M s₁ t₁ → Absorbs M s₂ t₂ → Absorbs M (s₁ + s₂) (t₁ + t₂)
The theorem `Absorbs.add` states that for any types `M` and `E`, given a bornology on `M`, two sets `s₁` and `s₂` of elements of type `E`, and two sets `t₁` and `t₂` also of elements of type `E`, and provided `E` is an additive zero class and there exists a distributive scalar multiplication of elements from `M` on `E`, if the set `s₁` absorbs the set `t₁` and the set `s₂` absorbs the set `t₂`, then the sum of sets `s₁` and `s₂` absorbs the sum of sets `t₁` and `t₂`. In mathematical terms, if `t₁` is contained in all scalings of `s₁` and `t₂` is contained in all scalings of `s₂` by all but a bounded set of elements of `M`, then `t₁ + t₂` is contained in all scalings of `s₁ + s₂` by all but a bounded set of elements of `M`.
More concisely: If bornologies on type `M`, sets `s₁`, `s₂` of type `E`, and sets `t₁`, `t₂` of type `E` satisfy `s₁ ⊆ λm, m • s₁ ∩ t₁` and `s₂ ⊆ λm, m • s₂ ∩ t₂`, and `M` is an additive zero class with distributive scalar multiplication, then `(s₁ ∪ s₂) ⊆ λm, m • ((s₁ ∪ s₂) ∩ (t₁ ∪ t₂))`.
|
absorbs_empty
theorem absorbs_empty :
∀ {M : Type u_1} {α : Type u_2} [inst : Bornology M] [inst_1 : SMul M α] {s : Set α}, Absorbs M s ∅
The theorem `absorbs_empty` states that for any types `M` and `α`, given a bornology on `M` and a scalar multiplication operation on `M` and `α`, any set `s` of type `α` absorbs the empty set. Here, absorbing is defined in the sense that the empty set is contained within all scalings of `s` by all but a bounded set of elements from `M`.
More concisely: For any bornology on type `M`, scalar multiplication on `M` and `α`, if a set `s` of type `α` absorbs any bounded subset of elements from `M`, then `s` absorbs the empty set.
|
Absorbent.subset
theorem Absorbent.subset :
∀ {M : Type u_1} {α : Type u_2} [inst : Bornology M] [inst_1 : SMul M α] {s t : Set α},
Absorbent M s → s ⊆ t → Absorbent M t
The theorem `Absorbent.subset` states that for any two sets `s` and `t` of any type `α` (where `α` has the scalar multiplication by a type `M` which has a bornology), if `s` is an absorbent set and every element of `s` is also in `t` (i.e., `s` is a subset of `t`), then `t` is also an absorbent set. In other words, the absorbency property is preserved under taking subsets.
More concisely: If `s` is an absorbent subset of `α` and `s` is contained in `t`, then `t` is also an absorbent subset of `α`.
|
Mathlib.Topology.Bornology.Absorbs._auxLemma.6
theorem Mathlib.Topology.Bornology.Absorbs._auxLemma.6 :
∀ {G₀ : Type u_1} {α : Type u_2} [inst : GroupWithZero G₀] [inst_1 : Bornology G₀] [inst_2 : MulAction G₀ α]
{s t : Set α}, Absorbs G₀ s t = ∀ᶠ (c : G₀) in Bornology.cobounded G₀, Set.MapsTo (fun x => c⁻¹ • x) t s
This theorem states that for any given types `G₀` and `α` where `G₀` is equipped with a GroupWithZero structure and a Bornology, and `α` has a multiplication action by `G₀`, a set `s` of type `α` absorbs another set `t` of type `α` if and only if for all `c` in the cobounded sets of `G₀` according to the Bornology, the function mapping `x` to `c⁻¹ • x` maps `t` into `s`. Here, `•` denotes the action of `G₀` on `α`, and `c⁻¹` is the multiplicative inverse of `c` in `G₀`.
More concisely: A set `s` of type `α` absorbs another set `t` of type `α` in the group `G₀` with Bornology if and only if for all cobounded elements `c` in `G₀`, the set `t` is mapped into `s` by the function `x mapsto c⁻¹ • x`.
|
Absorbs.of_neg_neg
theorem Absorbs.of_neg_neg :
∀ {M : Type u_1} {E : Type u_2} [inst : Monoid M] [inst_1 : AddGroup E] [inst_2 : DistribMulAction M E]
[inst_3 : Bornology M] {s t : Set E}, Absorbs M (-s) (-t) → Absorbs M s t
This theorem, referred to as the alias of the forward direction of `absorbs_neg_neg`, states that for any two sets `s` and `t` of a Type `E` which has an addition group structure, and a Type `M` that is a monoid and has a Bornology structure, if set `s` absorbs the negation of set `t` (`-t`), and set `M` absorbs the negation of set `s` (`-s`), then set `s` absorbs set `t` and set `M` absorbs set `s`. In other words, if the negative of `s` absorbs the negative of `t`, then `s` itself absorbs `t`. This is under a distributive multiplication action of `M` on `E`.
More concisely: If sets `s` and `t` in additive group `E` and monoid `M` with Bornology structure satisfy `-s absorption -t` and `-t absorption s`, then `s absorption t` holds under distributive multiplication action of `M` on `E`.
|
Absorbs.neg_neg
theorem Absorbs.neg_neg :
∀ {M : Type u_1} {E : Type u_2} [inst : Monoid M] [inst_1 : AddGroup E] [inst_2 : DistribMulAction M E]
[inst_3 : Bornology M] {s t : Set E}, Absorbs M s t → Absorbs M (-s) (-t)
The theorem `Absorbs.neg_neg` states that for any types `M` and `E`, given that `M` is a Monoid, `E` is an AddGroup, `M` is a DistribMulAction over `E`, and `M` has a Bornology structure, if a set `s` of type `E` absorbs another set `t` of the same type, then the negation of `s` also absorbs the negation of `t`. In other words, if `t` is contained in all scalings of `s` excluding a bounded set of elements, then `-t` will also be contained in all scalings of `-s` excluding a bounded set of elements.
More concisely: If sets `s` and `t` of an additive Abelian group `E` satisfy `t ⊆ ∑ (x : E) in s : E := {x} ⊤ − s`, then `-t ⊆ ∑ (x : E) in -s : E := {x} ⊤ − (-s)`. Here, `M` is a Monoid, `E` is an AddGroup, `M` is a DistribMulAction over `E`, and `M` has a Bornology structure.
|
Absorbs.mono_left
theorem Absorbs.mono_left :
∀ {M : Type u_1} {α : Type u_2} [inst : Bornology M] [inst_1 : SMul M α] {s₁ s₂ t : Set α},
Absorbs M s₁ t → s₁ ⊆ s₂ → Absorbs M s₂ t
The theorem `Absorbs.mono_left` states that for any types `M` and `α`, where `M` has a structure of Bornology and `α` has a structure of scalar multiplication (`SMul`) by `M`, given three sets `s₁`, `s₂`, and `t` of type `α`, if the set `s₁` absorbs the set `t`, and `s₁` is a subset of `s₂`, then it follows that `s₂` also absorbs `t`. In other words, the absorption property is monotonic on the left side: enlarging an absorbing set preserves the absorbing property.
More concisely: If `M` is a Bornology and `α` is an `SMul σ M`, and `s₁` absorbs `t` in `α` and `s₁` is a subset of `s₂`, then `s₂` absorbs `t`.
|
Absorbs.mono_right
theorem Absorbs.mono_right :
∀ {M : Type u_1} {α : Type u_2} [inst : Bornology M] [inst_1 : SMul M α] {s t₁ t₂ : Set α},
Absorbs M s t₁ → t₂ ⊆ t₁ → Absorbs M s t₂
The theorem `Absorbs.mono_right` states that for all types `M` and `α`, where `M` has a Bornology structure and `α` has a scalar multiplication structure, if a set `s` absorbs another set `t₁` and `t₂` is a subset of `t₁`, then `s` also absorbs `t₂`. Here, a set `s` absorbing another set `t` is defined such that `t` is contained in all scalings of `s` by all but a bounded set of elements in `M`.
More concisely: If `M` is a type with a Bornology structure, `α` is a type with a scalar multiplication structure, `s` absorbs `t₁`, and `t₂` is a subset of `t₁`, then `s` absorbs `t₂`.
|
Set.Finite.absorbs_sUnion
theorem Set.Finite.absorbs_sUnion :
∀ {M : Type u_1} {α : Type u_2} [inst : Bornology M] [inst_1 : SMul M α] {s : Set α} {T : Set (Set α)},
T.Finite → (Absorbs M s T.sUnion ↔ ∀ t ∈ T, Absorbs M s t)
The theorem `Set.Finite.absorbs_sUnion` states that for any types `M` and `α`, given a bornology on `M`, a scalar multiplication on `α`, a set `s` of `α`, and a set `T` of sets of `α`, if `T` is finite, then the set `s` absorbs the union of all sets in `T` if and only if `s` absorbs every set in `T`. Here, a set `s` absorbs another set `t` if every scaling of `s` by any but a bounded set of elements contains `t`, and a set is finite if it is equivalent to a set of natural numbers less than some natural number.
More concisely: For any bornology on a type `M`, scalar multiplication on a type `α`, finite set `T` of subsets of `α`, and set `s` of `α`, `s` absorbs the union of `T` if and only if it absorbs every set in `T`.
|
Set.Finite.absorbs_iUnion
theorem Set.Finite.absorbs_iUnion :
∀ {M : Type u_1} {α : Type u_2} [inst : Bornology M] [inst_1 : SMul M α] {s : Set α} {ι : Type u_3} {t : ι → Set α}
{I : Set ι}, I.Finite → (Absorbs M s (⋃ i ∈ I, t i) ↔ ∀ i ∈ I, Absorbs M s (t i))
The theorem `Set.Finite.absorbs_iUnion` states that for any types `M` and `α`, given a bornology on `M`, a scalar multiplication on `α`, a set `s` of type `α`, an index set `I` of type `ι` and a family `t` of sets of type `α` indexed by `ι`, if `I` is finite, then the set `s` absorbs the union of the family `t` over `I` if and only if `s` absorbs each member of the family `t` for every index in `I`. In other words, a set `s` absorbing a finite union of sets is equivalent to it absorbing each of the constituent sets individually. Here, 'absorbs' is used in the sense that set `s` absorbs another set if the latter is contained in all scalings of `s` by all but a bounded set of elements.
More concisely: For a bornology on type `M`, scalar multiplication on type `α`, finite index set `I`, set `s` of type `α`, and family `t` of sets of type `α` indexed by `I`, `s` absorbs the union of `t` if and only if it absorbs each member of `t` for every index in `I`.
|