Set.set_smul_subset_set_smul_iff
theorem Set.set_smul_subset_set_smul_iff :
∀ {α : Type u_2} {β : Type u_3} [inst : Group α] [inst_1 : MulAction α β] {A B : Set β} {a : α},
a • A ⊆ a • B ↔ A ⊆ B
This theorem states that for any two sets `A` and `B` of elements of some type `β` and any element `a` of type `α`, where `α` is a group and `β` is a set on which `α` acts multiplicatively, the scaled set `a • A` is a subset of the scaled set `a • B` if and only if `A` is a subset of `B`. In mathematical terms, given a group `α`, a set `β` with a group action defined by multiplication, and two subsets `A`, `B` of `β`, the condition `a • A ⊆ a • B` holds true if and only if `A ⊆ B`. Here `a • A` denotes the set of all elements obtained by scaling elements of `A` by `a`, and `a • B` is defined similarly.
More concisely: For any group action of a multiplicative group α on a set β, and subsets A, B of β, the condition a • A ⊆ a • B holds if and only if A ⊆ B.
|
Set.preimage_vadd
theorem Set.preimage_vadd :
∀ {α : Type u_2} {β : Type u_3} [inst : AddGroup α] [inst_1 : AddAction α β] (a : α) (t : Set β),
(fun x => a +ᵥ x) ⁻¹' t = -a +ᵥ t
The theorem `Set.preimage_vadd` states that for any type `α` which is an additive group, any type `β` on which `α` acts additively (in other words, `β` is an `α`-set, meaning `α` elements can be added to `β` elements), any element `a` of `α`, and any set `t` of elements of `β`, the preimage of `t` under the operation of vector addition with `a` equals the set obtained by adding the additive inverse of `a` to each element of `t`. In simpler words, if we translate all elements of `t` by `a` or by `-a` (the opposite of `a`), we end up with the same set.
More concisely: For any additive group α acting on a set β, the preimage of a set t under the translation by a element is equal to the set obtained by translating each element of t by the additive inverse of a.
|
Set.smul_set_inter
theorem Set.smul_set_inter :
∀ {α : Type u_2} {β : Type u_3} [inst : Group α] [inst_1 : MulAction α β] {s t : Set β} {a : α},
a • (s ∩ t) = a • s ∩ a • t
This theorem states that for any given types `α` and `β`, where `α` is a group and `β` is a set upon which `α` has a multiplication action, the scalar multiplication of an element `a` from `α` with the intersection of two sets `s` and `t` from `β`, is the same as the intersection of the scalar multiplication of `a` with `s` and the scalar multiplication of `a` with `t`. In mathematical terms, it says that for every group element `a` and sets `s` and `t` we have `a * (s ∩ t) = (a * s) ∩ (a * t)`. This expresses a distributive property of scalar multiplication over set intersection in the context of group actions.
More concisely: For any group action of type `α` on set `β`, the scalar multiplication of an element `a` from `α` with the intersection of sets `s` and `t` from `β` is equal to the intersection of the scalar multiplication of `a` with `s` and the scalar multiplication of `a` with `t`. In symbols, `a * (s ∩ t) = (a * s) ∩ (a * t)`.
|
Set.smul_subset_smul_right
theorem Set.smul_subset_smul_right :
∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {s₁ s₂ : Set α} {t : Set β}, s₁ ⊆ s₂ → s₁ • t ⊆ s₂ • t
The theorem `Set.smul_subset_smul_right` states that for any types `α` and `β` with a scalar multiplication operation (denoted `SMul α β`), given two sets `s₁` and `s₂` of type `α` and a set `t` of type `β`, if `s₁` is a subset of `s₂` (denoted `s₁ ⊆ s₂`), then the scalar multiplication of `s₁` and `t` is a subset of the scalar multiplication of `s₂` and `t` (denoted `s₁ • t ⊆ s₂ • t`). In other words, we are showing that scalar multiplication preserves the subset relation on the right.
More concisely: For sets `s₁ ⊆ s₂` of types `α` with a scalar multiplication operation `SMul α β`, `s₁ • t ⊆ s₂ • t` holds for any set `t` of type `β`.
|
Set.vadd_set_univ
theorem Set.vadd_set_univ :
∀ {α : Type u_2} {β : Type u_3} [inst : AddGroup α] [inst_1 : AddAction α β] {a : α}, a +ᵥ Set.univ = Set.univ := by
sorry
This theorem states that for any type `α` which has an `AddGroup` instance, any type `β` which has an `AddAction` instance of `α` on `β`, and any element `a` of type `α`, the operation of vector addition of `a` with the universal set on `β` (denoted by `a +ᵥ Set.univ`) yields the universal set on `β` itself. This means that adding any element of the `AddGroup` to all elements in the universal set does not change the set, which corresponds to the idea that adding a group element to every point in a space (acting on the space) does not change the overall space.
More concisely: For any `AddGroup` type `α`, any `AddAction` instance of `α` on type `β`, and any `α` element `a`, `a +ᵥ Set.univ = Set.univ` in type `β`.
|
Set.smul_mem_smul_set
theorem Set.smul_mem_smul_set :
∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {s : Set β} {a : α} {b : β}, b ∈ s → a • b ∈ a • s
The theorem `Set.smul_mem_smul_set` states that for any types `α` and `β`, where `α` has a scalar multiplication operation with `β`, given a set `s` of type `β`, a scalar `a` of type `α`, and an element `b` of type `β`, if `b` is an element of `s`, then the result of scalar multiplication of `a` and `b` (`a • b`) is an element of the scalar multiplication of `a` and the set `s` (`a • s`). In other words, for every element in a set, its scalar multiplication is an element in the scalar multiplication of the set.
More concisely: For any type `α` with scalar multiplication, set `β`, and `a ∈ α`, `b ∈ β`, if `b ∈ s`, then `a • b ∈ a • s` (scalar multiplication of an element by a set).
|
Set.set_smul_subset_set_smul_iff₀
theorem Set.set_smul_subset_set_smul_iff₀ :
∀ {α : Type u_2} {β : Type u_3} [inst : GroupWithZero α] [inst_1 : MulAction α β] {a : α},
a ≠ 0 → ∀ {A B : Set β}, a • A ⊆ a • B ↔ A ⊆ B
The theorem `Set.set_smul_subset_set_smul_iff₀` asserts that for any type `α` with a structure of a group with a nonzero element, and any type `β` with an action of `α`, given two sets `A` and `B` of type `β`, scalar multiplication of `A` and `B` by the same nonzero element `a` from `α` preserves the subset relation between `A` and `B`. In other words, if `a` is not zero, then `A` is a subset of `B` if and only if the set obtained by multiplying every element of `A` by `a` is a subset of the set obtained by multiplying every element of `B` by `a`.
More concisely: For any group `α` with a nonzero element and any `α`-module `β`, if sets `A ⊆ B` in `β`, then for all `a ≠ 0` in `α`, `aA ⊆ aB`.
|
Set.smul_set_empty
theorem Set.smul_set_empty : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {a : α}, a • ∅ = ∅
This theorem states that for any type `α` and `β` with a scalar multiplication (`SMul`) operation defined, when we multiply an empty set (`∅`) of type `β` by any element (`a`) of type `α`, the result is also the empty set (`∅`). This is analogous to multiplying zero by any number in normal arithmetic; the result is always zero.
More concisely: For any types `α` and `β` with a scalar multiplication operation, the empty set of type `β` is multiplicatively identic to the zero element of type `α`, i.e., `∅ * a = ∅` for all `a : α`.
|
Set.mem_inv_smul_set_iff₀
theorem Set.mem_inv_smul_set_iff₀ :
∀ {α : Type u_2} {β : Type u_3} [inst : GroupWithZero α] [inst_1 : MulAction α β] {a : α},
a ≠ 0 → ∀ (A : Set β) (x : β), x ∈ a⁻¹ • A ↔ a • x ∈ A
The theorem `Set.mem_inv_smul_set_iff₀` states for any two types `α` and `β`, where `α` is a group with zero and `β` is a set on which `α` acts multiplicatively, given any nonzero element `a` of `α`, a set `A` of `β`, and an element `x` of `β`, the element `x` is in the set obtained by scaling `A` by the multiplicative inverse of `a` if and only if the result of scaling `x` by `a` is in `A`.
In mathematical terms, for any types `α` and `β` with `α` a group with zero and `β` a `mul_action` of `α`, for any nonzero `a ∈ α`, set `A` of `β`, and `x ∈ β`, we have `x ∈ a⁻¹ • A` if and only if `a • x ∈ A`.
More concisely: For any group with zero `α`, set `β` with a multiplicative action by `α`, nonzero `a` in `α`, and set `A` in `β`, the element `x` in `β` belongs to the scaled set `a⁻¹ • A` if and only if `a • x` belongs to `A`.
|
Set.mem_smul_set_iff_inv_smul_mem
theorem Set.mem_smul_set_iff_inv_smul_mem :
∀ {α : Type u_2} {β : Type u_3} [inst : Group α] [inst_1 : MulAction α β] {A : Set β} {a : α} {x : β},
x ∈ a • A ↔ a⁻¹ • x ∈ A
This theorem states that for any types `α` and `β`, where `α` is a group and there is a multiplication action from `α` on `β`, given a set `A` of elements of type `β`, an element `a` of type `α`, and an element `x` of type `β`, `x` is in the set obtained by scaling `A` by `a` if and only if `a⁻¹` scaled by `x` is in `A`. Here, `a • A` means the set obtained by scaling every element of `A` by `a`, and `a⁻¹ • x` means `x` scaled by the inverse of `a`.
More concisely: For any group action of type `α` on `β`, and any set `A` of elements in `β`, an element `x` is in the set `a • A` if and only if `a⁻¹ • x` is in `A`.
|
Set.zero_smul_set
theorem Set.zero_smul_set :
∀ {α : Type u_2} {β : Type u_3} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMulWithZero α β] {s : Set β},
s.Nonempty → 0 • s = 0
The theorem `Set.zero_smul_set` states that for any nonempty set `s` of type `β` in a scalar multiplication with zero structure (`SMulWithZero α β`), if `α` and `β` are types with zero, then the scaling of the set `s` by zero results in a singleton set containing only the zero element of `β`. In other words, regardless of the elements in the nonempty set `s`, when you multiply `s` by zero, you get a set that only contains `0` from type `β`.
More concisely: For any nonempty set `s` in a scalar multiplication structure with types `α` and `β` having zero elements, the set `s` multiplied by zero is a singleton set containing the zero element of `β`.
|
Set.vadd_mem_vadd_set
theorem Set.vadd_mem_vadd_set :
∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {s : Set β} {a : α} {b : β}, b ∈ s → a +ᵥ b ∈ a +ᵥ s
The theorem `Set.vadd_mem_vadd_set` states that for any types `α` and `β` with a vector addition operation (`VAdd α β`), any set `s` of elements of type `β`, and any elements `a` of type `α` and `b` of type `β`, if `b` is an element of `s`, then the result of vector adding `a` and `b` (`a +ᵥ b`) is an element of the set resulting from vector adding `a` to every element of `s` (`a +ᵥ s`).
More concisely: If `a` is an element of type `α`, `b` is an element of set `s` of type `β`, and `β` has vector addition, then `a +ᵥ b` is an element of `a +ᵥ s`.
|
Set.smul_subset_smul_left
theorem Set.smul_subset_smul_left :
∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {s : Set α} {t₁ t₂ : Set β}, t₁ ⊆ t₂ → s • t₁ ⊆ s • t₂
The theorem `Set.smul_subset_smul_left` states that for any types `α` and `β`, where `β` is a set that can be scaled by elements of `α` (denoted as [inst : SMul α β]), and for any set `s` of type `α` and any sets `t₁` and `t₂` of type `β`, if `t₁` is a subset of `t₂`, then the scaled set `s • t₁` is a subset of the scaled set `s • t₂`. Here, `s • t₁` and `s • t₂` denote the sets resulting from the scalar multiplication of each element in `t₁` and `t₂` by each element in `s`, respectively.
More concisely: For any sets `s` of type `α` and `t₁, t₂` of type `β` with `β` being scalable by `α`, if `t₁` is a subset of `t₂`, then `s • t₁` is a subset of `s • t₂`.
|
Set.singleton_vadd
theorem Set.singleton_vadd : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {t : Set β} {a : α}, {a} +ᵥ t = a +ᵥ t
The theorem "Set.singleton_vadd" states that for any types `α` and `β` such that there is a vector addition operation defined on `α` and `β`, and for any set `t` of type `β` and any element `a` of type `α`, the vector addition of the singleton set containing `a` and `t` is equal to the vector addition of `a` and `t`. In mathematical terms, it states that for a singleton set `{a}` and a set `t`, the vector addition `{a} +ᵥ t` is the same as `a +ᵥ t`.
More concisely: For sets `{a}` (a singleton) and `t` in types `α` and `β` respectively with defined vector addition, the operation `{a} +ᵥ t` equals `a +ᵥ t`.
|
Set.mem_smul_set_iff_inv_smul_mem₀
theorem Set.mem_smul_set_iff_inv_smul_mem₀ :
∀ {α : Type u_2} {β : Type u_3} [inst : GroupWithZero α] [inst_1 : MulAction α β] {a : α},
a ≠ 0 → ∀ (A : Set β) (x : β), x ∈ a • A ↔ a⁻¹ • x ∈ A
This theorem states that for any types `α` and `β`, given `α` as a group with zero and `β` as a set on which `α` acts multiplicatively, for any non-zero element `a` of `α`, any set `A` of `β`, and any element `x` of `β`, `x` is an element of the set `A` scaled by `a` if and only if the inverse of `a` scaled by `x` is an element of `A`. This provides a characterization for membership of a point in a scaled set in terms of the action of the inverse of the scaling factor on the point.
More concisely: For any group `α` with zero, set `β`, and non-zero `a` in `α`, an element `x` in `β` belongs to the set `A` scaled by `a` if and only if the inverse of `a` scaled by `x` belongs to `A`.
|
Set.smul_mem_smul_set_iff
theorem Set.smul_mem_smul_set_iff :
∀ {α : Type u_2} {β : Type u_3} [inst : Group α] [inst_1 : MulAction α β] {s : Set β} {a : α} {x : β},
a • x ∈ a • s ↔ x ∈ s
This theorem states that for any type `α` that forms a group, and any type `β` that has a multiplication action by `α`, if we have a set `s` of elements of type `β`, an element `a` from group `α`, and an element `x` from type `β`, then `x` is in `s` if and only if the result of `a` acting on `x` (denoted by `a • x`) is in the set resulting from `a` acting on every element of `s` (denoted by `a • s`). This theorem essentially captures the invariance of set membership under the action of a group.
More concisely: For any set `s` of elements from a group action `α` on type `β`, an element `x` is in `s` if and only if `a • x` is in `a • s` for all `a` in `α`.
|
Set.vadd_subset_vadd_right
theorem Set.vadd_subset_vadd_right :
∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {s₁ s₂ : Set α} {t : Set β}, s₁ ⊆ s₂ → s₁ +ᵥ t ⊆ s₂ +ᵥ t := by
sorry
This theorem, `Set.vadd_subset_vadd_right`, states that for any types `α` and `β` where `α` has a vector addition operation (`VAdd α β`), given any two sets `s₁` and `s₂` of type `α`, and another set `t` of type `β`, if `s₁` is a subset of `s₂` (`s₁ ⊆ s₂`), then the set formed by adding each element of `s₁` to each element of `t` (`s₁ +ᵥ t`) is also a subset of the set formed by adding each element of `s₂` to each element of `t` (`s₂ +ᵥ t`).
More concisely: For any types `α` with vector addition and sets `s₁ ⊆ s₂` of `α`, `s₁ ⊆ s₂ +ᵥ t` holds for any set `t`.
|
Set.smul_set_univ
theorem Set.smul_set_univ :
∀ {α : Type u_2} {β : Type u_3} [inst : Group α] [inst_1 : MulAction α β] {a : α}, a • Set.univ = Set.univ := by
sorry
This theorem states that for any given types `α` and `β`, where `α` is a group and there is a multiplicative action defined from `α` to `β`, the scaled universal set `a • Set.univ` (where `a` is an element of the group `α` and `•` is the scalar multiplication operation) is equivalent to the universal set `Set.univ`. The universal set in this context is the set containing all elements of the type `β`. In other words, scaling the universal set by any factor from the group does not change the set.
More concisely: For any group `α` and type `β`, the scalar multiplication of the universal set `Set.univ` by any element `a` from the group `α` results in the same set. In symbols: `a • Set.univ = Set.univ`.
|
Set.vadd_set_inter
theorem Set.vadd_set_inter :
∀ {α : Type u_2} {β : Type u_3} [inst : AddGroup α] [inst_1 : AddAction α β] {s t : Set β} {a : α},
a +ᵥ s ∩ t = (a +ᵥ s) ∩ (a +ᵥ t)
This theorem expresses a property in the context of additive group actions. It states that for any types `α` and `β`, where `α` is an additive group and `β` is a set acted upon by `α` (known as an `AddAction`), and given any two sets `s` and `t` of type `β` and an element `a` of type `α`, the set obtained by the group action of `a` on the intersection of `s` and `t` is equal to the intersection of the set obtained by the group action of `a` on `s` and the set obtained by the group action of `a` on `t`. In other words, this theorem says that the operation of adding a group element to a set and taking intersections commute with each other.
More concisely: For any additive group `α` and a set `β` acted upon by `α`, the group action commutes with intersections, that is, for any sets `s` and `t` in `β` and an element `a` in `α`, we have `a∘(s ∩ t) = (a∘s) ∩ (a∘t)`.
|
Set.smul_mem_smul
theorem Set.smul_mem_smul :
∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {s : Set α} {t : Set β} {a : α} {b : β},
a ∈ s → b ∈ t → a • b ∈ s • t
This theorem states that for any two types `α` and `β` where `β` is a scalar multiplication space over `α`, and given two sets `s` of type `α` and `t` of type `β`, and two elements `a` from `s` and `b` from `t`, if `a` belongs to `s` and `b` belongs to `t`, then the result of the scalar multiplication of `a` and `b` (denoted as `a • b`) belongs to the set created by the scalar multiplication of `s` and `t` (denoted as `s • t`). In mathematical terms, if `a ∈ s` and `b ∈ t`, then `a • b ∈ s • t`.
More concisely: For any types `α` and `β` with `β` a scalar multiplication space over `α`, and sets `s` of type `α` and `t` of type `β`, if `a ∈ s` and `b ∈ t`, then `a • b ∈ s • t`.
|
Set.smul_set_subset_iff
theorem Set.smul_set_subset_iff :
∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {s t : Set β} {a : α}, a • s ⊆ t ↔ ∀ ⦃b : β⦄, b ∈ s → a • b ∈ t
The theorem `Set.smul_set_subset_iff` states that for any types `α` and `β` with a scalar multiplication operation (`SMul α β`), given sets `s` and `t` of type `β` and a scalar `a` of type `α`, the scalar multiplication of the set `s` by `a` is a subset of `t` if and only if for every element `b` in `s`, the result of scalar multiplying `b` by `a` is in `t`. This basically means that if we multiply each element of `s` by `a` and all these results are also elements of `t`, then the set formed by multiplying all elements of `s` by `a` is a subset of `t`.
More concisely: For sets $s$ and $t$ of type $\beta$ and a scalar $a$ of type $\alpha$ in a type with scalar multiplication, $a \cdot s \subseteq t$ if and only if for all $b \in s$, $a \cdot b \in t$.
|
Set.preimage_smul_inv
theorem Set.preimage_smul_inv :
∀ {α : Type u_2} {β : Type u_3} [inst : Group α] [inst_1 : MulAction α β] (a : α) (t : Set β),
(fun x => a⁻¹ • x) ⁻¹' t = a • t
This theorem, `Set.preimage_smul_inv`, states that for any types `α` and `β` where `α` is a group and `β` has a multiplication action by `α`, and for any element `a` of `α` and a set `t` of `β`, the preimage of the set `t` under the function `(fun x => a⁻¹ • x)` (which maps each element `x` of `β` to the product of the inverse of `a` and `x`) is equal to the set obtained by scaling all elements of `t` by `a`. In terms of group actions, this theorem describes how the preimage under the action of an inverse element corresponds to the original set scaled by the element itself.
More concisely: For any group `α` acting on a set `β` and any `a in α` and set `t in β`, the preimage of `t` under the function `x => a⁻¹ • x` is equal to the set obtained by scaling `t` by `a`.
|
Set.mem_smul_set
theorem Set.mem_smul_set :
∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {t : Set β} {a : α} {x : β}, x ∈ a • t ↔ ∃ y ∈ t, a • y = x := by
sorry
This theorem states that for any types `α` and `β` where `α` has a scalar multiplication operation with `β`, any set `t` of type `β`, any element `a` of type `α`, and any element `x` of type `β`, `x` belongs to the scalar multiplication of `a` and `t` if and only if there exists an element `y` in `t` such that `a` scaled by `y` equals `x`. In mathematical terms, for any scalar `a` and any set `t`, an element `x` belongs to the scalar multiplication of `a` and `t` (`a∙t`) if and only if there's an element `y` in `t` such that `a∙y = x`.
More concisely: For any scalar `a` and set `t`, an element `x` belongs to the scalar multiplication of `a` and `t` if and only if there exists an element `y` in `t` such that `a` scalar-multiplies `y` to obtain `x`. In Lean notation, `a ⊤ t = { y : β | ∃ (y' : β), a * y' = x }`.
|
Set.image_smul
theorem Set.image_smul :
∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {t : Set β} {a : α}, (fun x => a • x) '' t = a • t
The theorem `Set.image_smul` states that for any types `α` and `β` with a scalar multiplication operation defined on them (`SMul α β`), any set `t` of type `β`, and any element `a` of type `α`, the image of set `t` under the function that multiplies each element by `a` (expressed as `(fun x => a • x) '' t`) is equal to the scalar multiplication of `a` and the entire set `t` (expressed as `a • t`). Essentially, this theorem formalizes the distribution of scalar multiplication over a set in the context of image of a set under a function.
More concisely: For any type `α` and `β` with scalar multiplication, and for any set `t` of type `β` and element `a` of type `α`, `(fun x => a • x) '' t = a • t`.
|
Mathlib.Data.Set.Pointwise.SMul._auxLemma.36
theorem Mathlib.Data.Set.Pointwise.SMul._auxLemma.36 :
∀ {α : Type u_2} [inst : InvolutiveNeg α] {s : Set α}, -s = Neg.neg '' s
This theorem states that for any type `α` that is equipped with an `InvolutiveNeg` structure (which is a structure that has a negation operation `neg` such that negating twice yields the original element), and for any set `s` of type `α`, the negation of the set `s` (denoted by `-s`) is equal to the image of the set `s` under the negation operation `Neg.neg` (denoted by `Neg.neg '' s`).
In mathematical terms, this theorem asserts that every element in the set `-s` is the negative of some element in the set `s`, and vice versa. Hence, the set `-s` is precisely the set of negatives of elements of `s`.
More concisely: For any set `s` of a type `α` equipped with an `InvolutiveNeg` structure, `-s` = `Neg.neg '' s`, where `-s` denotes the negation of the set `s` and `Neg.neg '' s` is the image of `s` under the negation operation.
|
Set.mem_vadd_set_iff_neg_vadd_mem
theorem Set.mem_vadd_set_iff_neg_vadd_mem :
∀ {α : Type u_2} {β : Type u_3} [inst : AddGroup α] [inst_1 : AddAction α β] {A : Set β} {a : α} {x : β},
x ∈ a +ᵥ A ↔ -a +ᵥ x ∈ A
This theorem states that for any types `α` and `β`, where `α` is an additive group and there is an additive action of `α` on `β`, and any set `A` of type `β`, and any elements `a` in `α` and `x` in `β`, `x` is in the translated set `a +ᵥ A` if and only if the element `-a +ᵥ x` is in the set `A`. Here, `+ᵥ` denotes the operation of translating a set or an element by adding an element of the additive group.
More concisely: For any additive group `α` acting on type `β`, and any set `A` of type `β` and elements `a in α` and `x in β`, the element `x` is in the translated set `a +ᵥ A` if and only if `-a +ᵥ x` is in `A`.
|
Set.smul_set_mono
theorem Set.smul_set_mono :
∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {s t : Set β} {a : α}, s ⊆ t → a • s ⊆ a • t
The theorem `Set.smul_set_mono` states that for all types `α` and `β`, when `β` is a scalar multiplication (`SMul`) of `α`, given two sets `s` and `t` of type `β` and an element `a` of type `α`, if set `s` is a subset of set `t` (`s ⊆ t`), then the scalar multiplication of `a` and set `s` (`a • s`) is a subset of the scalar multiplication of `a` and set `t` (`a • t`). Essentially, scalar multiplication preserves the subset relationship between two sets.
More concisely: For all types `α` and `β` (where `β` is a scalar multiplication of `α`), if `s ⊆ t` are sets of type `β` and `a` is an element of type `α`, then `a • s ⊆ a • t`. (Scalar multiplication preserves subset relationships between sets.)
|
Set.set_smul_subset_iff
theorem Set.set_smul_subset_iff :
∀ {α : Type u_2} {β : Type u_3} [inst : Group α] [inst_1 : MulAction α β] {A B : Set β} {a : α},
a • A ⊆ B ↔ A ⊆ a⁻¹ • B
The theorem `Set.set_smul_subset_iff` states that for any types `α` and `β`, where `α` is a group and `β` is a set on which `α` acts (mulitplicatively), for any sets `A` and `B` of type `β`, and for any element `a` of the group `α`, the scalar multiplication of `a` and `A` is a subset of `B` if and only if `A` is a subset of the scalar multiplication of the inverse of `a` and `B`.
In mathematical terms, this theorem states that for all elements `a` in a group `α`, and for all subsets `A` and `B` of a set `β` on which `α` acts, $aA \subseteq B$ if and only if $A \subseteq a^{-1}B$.
More concisely: For any group `α` acting multiplicatively on a set `β`, and for all `a` in `α` and subsets `A` and `B` of `β`, $aA \subseteq B$ if and only if $A \subseteq a^{-1}B$.
|
Set.preimage_smul_inv₀
theorem Set.preimage_smul_inv₀ :
∀ {α : Type u_2} {β : Type u_3} [inst : GroupWithZero α] [inst_1 : MulAction α β] {a : α},
a ≠ 0 → ∀ (t : Set β), (fun x => a⁻¹ • x) ⁻¹' t = a • t
This theorem, denoted as `Set.preimage_smul_inv₀`, states that for any types `α` and `β`, given a `GroupWithZero` instance for `α` and a `MulAction` instance between `α` and `β`. If we have a non-zero element `a` in `α` and a set `t` of type `β`, then the preimage of the set `t` under the function `(fun x => a⁻¹ • x)` is equal to the set obtained by scaling `t` by `a`. In other words, if we scale each element in `t` by the inverse of `a` and then calculate the preimages, we get the same result as if we had directly scaled the set `t` by `a`.
In terms of mathematical notation, this can be expressed as: for all $a \in \alpha$ such that $a \neq 0$ and for all sets $t \subset \beta$, we have $(f^{-1}(t) = a \cdot t)$ where $f(x) = a^{-1} \cdot x$.
More concisely: For any non-zero element `a` in a group with zero `α` and a set `t` in `β`, the preimage of `t` under the function `x ↔ a⁻¹ * x` is equal to the set obtained by scaling `t` by `a`.
|
Set.set_smul_subset_iff₀
theorem Set.set_smul_subset_iff₀ :
∀ {α : Type u_2} {β : Type u_3} [inst : GroupWithZero α] [inst_1 : MulAction α β] {a : α},
a ≠ 0 → ∀ {A B : Set β}, a • A ⊆ B ↔ A ⊆ a⁻¹ • B
This theorem is about the interaction between scalar multiplication and subset relations in the context of a group with zero and a multiplicative action. Specifically, for any types `α` and `β` where `α` is a group with zero and `β` has a multiplication action by `α`, and for any non-zero `a` of type `α` and sets `A` and `B` of type `β`, the statement asserts that the set obtained by scalar multiplying `A` by `a` is a subset of `B` if and only if `A` is a subset of the set obtained by scalar multiplying `B` by the inverse of `a`. In mathematical notation, this can be written as: $aA \subseteq B$ if and only if $A \subseteq a^{-1}B$.
More concisely: For any group with zero `α`, type `β` with a multiplicative action by `α`, non-zero `a` in `α`, and sets `A` and `B` in `β`, $aA \subseteq B$ if and only if $A \subseteq a^{-1}B$.
|
Mathlib.Data.Set.Pointwise.SMul._auxLemma.15
theorem Mathlib.Data.Set.Pointwise.SMul._auxLemma.15 :
∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {s : Set α} {t : Set β} {b : β},
(b ∈ s • t) = ∃ x ∈ s, ∃ y ∈ t, x • y = b
This theorem states that for any types `α` and `β` with a scalar multiplication operation `•` defined between them, given sets `s` of type `α` and `t` of type `β`, and an element `b` of type `β`, the element `b` belongs to the scalar multiplication of set `s` and set `t` (denoted as `s • t`) if and only if there exist an element `x` in set `s` and an element `y` in set `t` such that the scalar multiplication of `x` and `y` equals `b`. Here, `s • t` refers to the set of all elements that can be obtained by multiplying an element from `s` with an element from `t`.
More concisely: For any types `α` and `β` with scalar multiplication `•` and sets `s` of type `α` and `t` of type `β`, `b ∈ s • t` if and only if there exist `x ∈ s` and `y ∈ t` such that `x • y = b`.
|
Set.smul_set_neg
theorem Set.smul_set_neg :
∀ {α : Type u_2} {β : Type u_3} [inst : Monoid α] [inst_1 : AddGroup β] [inst_2 : DistribMulAction α β] (a : α)
(t : Set β), a • -t = -(a • t)
The theorem `Set.smul_set_neg` states that for any type `α` with a monoid structure, another type `β` with an additive group structure, and a distributive multiplicative action of `α` on `β`, given an element `a` of type `α` and a set `t` of type `β`, the scalar multiplication of `a` with the additive inverse of `t` (`-t`) is equal to the additive inverse of the scalar multiplication of `a` with `t`. In mathematical terms, this is `a • (-t) = - (a • t)`. This assertion formalizes the compatibility between scalar multiplication and negation operation in the context of distributed multiplicative action.
More concisely: For any monoid `α`, additive group `β`, and distributive multiplicative action of `α` on `β`, we have `a * (-t) = - (a * t)` for all `a ∈ α` and `t ∈ β`.
|
Set.vsub_self_mono
theorem Set.vsub_self_mono : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] {s t : Set β}, s ⊆ t → s -ᵥ s ⊆ t -ᵥ t
This theorem, `Set.vsub_self_mono`, states that for any types `α` and `β`, if `α` has a vector subtraction structure (`VSub`), and `s` and `t` are sets of type `β`, then if `s` is a subset of `t`, it follows that the vector difference of `s` with itself (`s -ᵥ s`) is a subset of the vector difference of `t` with itself (`t -ᵥ t`). This theorem essentially guarantees that taking vector differences of sets respects the subset relation.
More concisely: If `α` has a vector subtraction structure and `s` is a subset of `t` in type `β`, then `s -ᵥ s` is a subset of `t -ᵥ t`.
|
Set.preimage_smul
theorem Set.preimage_smul :
∀ {α : Type u_2} {β : Type u_3} [inst : Group α] [inst_1 : MulAction α β] (a : α) (t : Set β),
(fun x => a • x) ⁻¹' t = a⁻¹ • t
This theorem asserts that, for any types `α` and `β` where `α` is a group and `β` is an object of `α`'s action, and given any element `a` from `α` and set `t` of `β`, the preimage of `t` under the function that maps `x` to `a` multiplied by `x` is equal to the set of elements obtained by multiplying `a⁻¹` with each element of `t`. In mathematical terms, this theorem states that for a group action, the preimage of a set under scalar multiplication is equal to scalar multiplication by the inverse element in the group.
More concisely: For any group action of type `α` on type `β`, the preimage of a set `t` under the scalar multiplication by an element `a` from `α` is equal to the set of elements obtained by scaling each element `x` in `t` with the inverse `a⁻¹` of `a`. In other words, `a⁺¹⁇{x | x ∈ t} = {a⁻¹ * x | x ∈ t}`.
|
Set.smul_set_iUnion
theorem Set.smul_set_iUnion :
∀ {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [inst : SMul α β] (a : α) (s : ι → Set β),
a • ⋃ i, s i = ⋃ i, a • s i
The theorem `Set.smul_set_iUnion` states that for all types α and β, for all sort ι, given an instance of scalar multiplication (`SMul`) on α and β, a scalar `a` of type α and a function `s` from ι to a set of β, the scalar multiplication of `a` with the union (over some index set ι) of the sets `s i` is equal to the union of the scalar multiplication of `a` with each individual set `s i`. In mathematical terms, this can be written as \(a \cdot \bigcup_{i} s_i = \bigcup_{i} a \cdot s_i\).
More concisely: For any types α and β with scalar multiplication, and for any function from an index set to sets of β, the scalar multiplication of an element by the union of the sets is equal to the union of the scalar multiplications of that element by each set. In other words, \(a \cdot \bigcup\_{i} s\_i = \bigcup\_{i} a \cdot s\_i\).
|
Set.subset_set_smul_iff₀
theorem Set.subset_set_smul_iff₀ :
∀ {α : Type u_2} {β : Type u_3} [inst : GroupWithZero α] [inst_1 : MulAction α β] {a : α},
a ≠ 0 → ∀ {A B : Set β}, A ⊆ a • B ↔ a⁻¹ • A ⊆ B
This theorem, `Set.subset_set_smul_iff₀`, is a statement about the interaction of sets and scalar multiplication in the context of a group with zero. Specifically, given two types `α` and `β` where `α` is a group with zero and `β` supports multiplication action by `α`, and given two sets `A` and `B` of type `β`, the theorem states that for any nonzero element `a` of `α`, the set `A` is a subset of the set resulting from scalar multiplication of `B` by `a` if and only if the set resulting from scalar multiplication of `A` by the inverse of `a` is a subset of `B`. In other words, it provides a condition for the scalar multiplication of a set to be subset of another set. This theorem characterizes the "subset" relation in terms of scalar multiplication in the setting of a group with zero.
More concisely: For sets `A` and `B` of a group `α` with zero, and a nonzero element `a` in `α`, `A ⊆ {b ∈ β | ∃ x ∈ A, b = ax}` if and only if `{b ∈ β | ∃ x ∈ A, b = x/a} ⊆ B`.
|
Set.smul_mem_smul_set_iff₀
theorem Set.smul_mem_smul_set_iff₀ :
∀ {α : Type u_2} {β : Type u_3} [inst : GroupWithZero α] [inst_1 : MulAction α β] {a : α},
a ≠ 0 → ∀ (A : Set β) (x : β), a • x ∈ a • A ↔ x ∈ A
This theorem states that for any arbitrary types `α` and `β`, where `α` is a group with zero and `β` is an `α`-module, and given any non-zero element `a` from `α`, any set `A` of elements of type `β`, and any element `x` from `β`, the scaled element `a • x` is an element of the scaled set `a • A` if and only if `x` is an element of `A`. This theorem establishes a correspondence between an element's membership in a set and that of its scaled version in the scaled set, under the condition that the scaling factor is non-zero.
More concisely: For any group `α` with zero, `α`-module `β`, and non-zero `a` in `α`, an element `x` in `β` belongs to the scaled set `a • A` if and only if `x` is in `A`.
|
Set.preimage_vadd_neg
theorem Set.preimage_vadd_neg :
∀ {α : Type u_2} {β : Type u_3} [inst : AddGroup α] [inst_1 : AddAction α β] (a : α) (t : Set β),
(fun x => -a +ᵥ x) ⁻¹' t = a +ᵥ t
This theorem states that for any type `α` that forms an additive group, any type `β` that `α` acts upon (i.e., there exists an action of `α` on `β`), any element `a` of type `α`, and any set `t` of type `β`, the preimage of the set `t` under the function that adds the negation of `a` to each element (`fun x => -a +ᵥ x`) is the same as the set obtained by adding `a` to each element of `t`. Here, "`+ᵥ`" denotes the action of the additive group `α` on `β`, and "preimage" refers to the set of all elements in the domain that are mapped to the elements of `t` by the function.
More concisely: For any additive group `α` acting on type `β`, and for any `a` in `α` and set `t` in `β`, the preimage of `t` under `x ↔- a + x` is equal to `a + t`.
|
Set.mem_inv_smul_set_iff
theorem Set.mem_inv_smul_set_iff :
∀ {α : Type u_2} {β : Type u_3} [inst : Group α] [inst_1 : MulAction α β] {A : Set β} {a : α} {x : β},
x ∈ a⁻¹ • A ↔ a • x ∈ A
This theorem is stating that for any two types `α` and `β`, where `α` has a group structure and `β` has a multiplication action by `α`, for any set `A` of elements of type `β`, any element `a` of type `α`, and any element `x` of type `β`, `x` is in the set obtained by multiplying each element of `A` by `a⁻¹` if and only if the element obtained by multiplying `a` and `x` is in `A`. In mathematical terms, for any group `α`, any `α`-set `β`, any subset `A` of `β`, any element `a` in `α`, and any element `x` in `β`, we have that `x ∈ a⁻¹ • A` if and only if `a • x ∈ A`.
More concisely: For any group `α`, `α`-set `β`, subset `A` of `β`, element `a` in `α`, and `x` in `β`, `x` is in the set of elements obtained by taking the inverse of `a`-action on `A` if and only if the element obtained by multiplying `a` and `x` is in `A`.
|
Set.subset_set_smul_iff
theorem Set.subset_set_smul_iff :
∀ {α : Type u_2} {β : Type u_3} [inst : Group α] [inst_1 : MulAction α β] {A B : Set β} {a : α},
A ⊆ a • B ↔ a⁻¹ • A ⊆ B
This theorem is about subsets and scalar multiplication in the context of sets and groups. Given a set `A` and `B` of elements of some type `β` which has a group action defined by a group `α`, and an element `a` of group `α`, the theorem states that `A` is a subset of the scalar multiplication of `a` and `B` if and only if the scalar multiplication of the inverse of `a` and `A` is a subset of `B`. Here, the 'scalar multiplication' denotes the action of the group `α` on the set `β`.
More concisely: For sets `A` and `B` of elements of type `β` with a group action by `α`, and an element `a` in `α`, the sets `A` and `a⁻¹(B)` are equal if and only if `A` is a subset of `a · B` (scalar multiplication).
|