Pointwise operations of sets #
This file defines pointwise algebraic operations on sets.
Main declarations #
For sets s and t and scalar a:
s * t: Multiplication, set of allx * ywherex ∈ sandy ∈ t.s + t: Addition, set of allx + ywherex ∈ sandy ∈ t.s⁻¹: Inversion, set of allx⁻¹wherex ∈ s.-s: Negation, set of all-xwherex ∈ s.s / t: Division, set of allx / ywherex ∈ sandy ∈ t.s - t: Subtraction, set of allx - ywherex ∈ sandy ∈ t.s • t: Scalar multiplication, set of allx • ywherex ∈ sandy ∈ t.s +ᵥ t: Scalar addition, set of allx +ᵥ ywherex ∈ sandy ∈ t.s -ᵥ t: Scalar subtraction, set of allx -ᵥ ywherex ∈ sandy ∈ t.a • s: Scaling, set of alla • xwherex ∈ s.a +ᵥ s: Translation, set of alla +ᵥ xwherex ∈ s.
For α a semigroup/monoid, set α is a semigroup/monoid.
As an unfortunate side effect, this means that n • s, where n : ℕ, is ambiguous between
pointwise scaling and repeated pointwise addition; the former has (2 : ℕ) • {1, 2} = {2, 4}, while
the latter has (2 : ℕ) • {1, 2} = {2, 3, 4}.
We define set_semiring α, an alias of set α, which we endow with ∪ as addition and * as
multiplication. If α is a (commutative) monoid, set_semiring α is a (commutative) semiring.
Appropriate definitions and results are also transported to the additive theory via to_additive.
Implementation notes #
- The following expressions are considered in simp-normal form in a group:
(λ h, h * g) ⁻¹' s,(λ h, g * h) ⁻¹' s,(λ h, h * g⁻¹) ⁻¹' s,(λ h, g⁻¹ * h) ⁻¹' s,s * t,s⁻¹,(1 : set _)(and similarly for additive variants). Expressions equal to one of these will be simplified. - We put all instances in the locale
pointwise, so that these instances are not available by default. Note that we do not mark them as reducible (as argued by note [reducible non-instances]) since we expect the locale to be open whenever the instances are actually used (and making the instances reducible changes the behavior ofsimp.
Tags #
set multiplication, set addition, pointwise addition, pointwise multiplication, pointwise subtraction
0/1 as sets #
@[protected, instance]
The set (1 : set α) is defined as {1} in locale pointwise.
Equations
- set.has_one = {one := {1}}
@[protected, instance]
The set (0 : set α) is defined as {0} in locale pointwise.
Equations
- set.has_zero = {zero := {0}}
@[simp]
@[simp]
Set addition/multiplication #
@[protected, instance]
The set (s * t : set α) is defined as {x * y | x ∈ s, y ∈ t} in locale pointwise.
Equations
@[protected, instance]
The set (s + t : set α) is defined as {x + y | x ∈ s, y ∈ t} in locale pointwise.
Equations
@[simp]
theorem
set.image2_mul
{α : Type u_2}
{s t : set α}
[has_mul α] :
set.image2 has_mul.mul s t = s * t
@[simp]
theorem
set.image2_add
{α : Type u_2}
{s t : set α}
[has_add α] :
set.image2 has_add.add s t = s + t
@[simp]
theorem
set.singleton_add
{α : Type u_2}
{t : set α}
{a : α}
[has_add α] :
{a} + t = has_add.add a '' t
@[simp]
theorem
set.singleton_mul
{α : Type u_2}
{t : set α}
{a : α}
[has_mul α] :
{a} * t = has_mul.mul a '' t
@[simp]
theorem
set.singleton_add_hom_apply
{α : Type u_2}
[has_add α]
(ᾰ : α) :
⇑set.singleton_add_hom ᾰ = {ᾰ}
@[simp]
theorem
set.singleton_mul_hom_apply
{α : Type u_2}
[has_mul α]
(ᾰ : α) :
⇑set.singleton_mul_hom ᾰ = {ᾰ}
@[simp]
theorem
set.image_op_add
{α : Type u_2}
{s t : set α}
[has_add α] :
add_opposite.op '' (s + t) = add_opposite.op '' t + add_opposite.op '' s
@[simp]
theorem
set.image_op_mul
{α : Type u_2}
{s t : set α}
[has_mul α] :
mul_opposite.op '' s * t = (mul_opposite.op '' t) * mul_opposite.op '' s
@[simp]
theorem
set.image_add_left
{α : Type u_2}
{t : set α}
{a : α}
[add_group α] :
has_add.add a '' t = has_add.add (-a) ⁻¹' t
@[simp]
theorem
set.image_mul_left
{α : Type u_2}
{t : set α}
{a : α}
[group α] :
has_mul.mul a '' t = has_mul.mul a⁻¹ ⁻¹' t
@[simp]
theorem
set.preimage_mul_left_singleton
{α : Type u_2}
{a b : α}
[group α] :
has_mul.mul a ⁻¹' {b} = {a⁻¹ * b}
@[simp]
theorem
set.preimage_add_left_singleton
{α : Type u_2}
{a b : α}
[add_group α] :
has_add.add a ⁻¹' {b} = {-a + b}
@[simp]
@[simp]
theorem
set.preimage_add_left_zero
{α : Type u_2}
{a : α}
[add_group α] :
has_add.add a ⁻¹' 0 = {-a}
@[protected, instance]
set α is an add_zero_class under pointwise operations if α is.
Equations
- set.add_zero_class = {zero := 0, add := has_add.add set.has_add, zero_add := _, add_zero := _}
@[protected, instance]
set α is a mul_one_class under pointwise operations if α is.
Equations
- set.mul_one_class = {one := 1, mul := has_mul.mul set.has_mul, one_mul := _, mul_one := _}
@[protected, instance]
set α is an add_semigroup under pointwise operations if α is.
Equations
- set.add_semigroup = {add := has_add.add set.has_add, add_assoc := _}
@[protected, instance]
set α is a semigroup under pointwise operations if α is.
Equations
- set.semigroup = {mul := has_mul.mul set.has_mul, mul_assoc := _}
@[protected, instance]
set α is an add_comm_semigroup under pointwise operations if α is.
Equations
- set.add_comm_semigroup = {add := add_semigroup.add set.add_semigroup, add_assoc := _, add_comm := _}
@[protected, instance]
set α is a comm_semigroup under pointwise operations if α is.
Equations
- set.comm_semigroup = {mul := semigroup.mul set.semigroup, mul_assoc := _, mul_comm := _}
@[protected, instance]
set α is a monoid under pointwise operations if α is.
Equations
- set.monoid = {mul := semigroup.mul set.semigroup, mul_assoc := _, one := mul_one_class.one set.mul_one_class, one_mul := _, mul_one := _, npow := npow_rec (mul_one_class.to_has_mul (set α)), npow_zero' := _, npow_succ' := _}
@[protected, instance]
set α is an add_monoid under pointwise operations if α is.
Equations
- set.add_monoid = {add := add_semigroup.add set.add_semigroup, add_assoc := _, zero := add_zero_class.zero set.add_zero_class, zero_add := _, add_zero := _, nsmul := nsmul_rec (add_zero_class.to_has_add (set α)), nsmul_zero' := _, nsmul_succ' := _}
@[protected, instance]
set α is a comm_monoid under pointwise operations if α is.
Equations
- set.comm_monoid = {mul := monoid.mul set.monoid, mul_assoc := _, one := monoid.one set.monoid, one_mul := _, mul_one := _, npow := monoid.npow set.monoid, npow_zero' := _, npow_succ' := _, mul_comm := _}
@[protected, instance]
set α is an add_comm_monoid under pointwise operations if α is.
Equations
- set.add_comm_monoid = {add := add_monoid.add set.add_monoid, add_assoc := _, zero := add_monoid.zero set.add_monoid, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul set.add_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _}
theorem
set.nsmul_mem_nsmul
{α : Type u_2}
{s : set α}
{a : α}
[add_monoid α]
(ha : a ∈ s)
(n : ℕ) :
@[protected, instance]
def
set.decidable_mem_mul
{α : Type u_2}
{s t : set α}
[monoid α]
[fintype α]
[decidable_eq α]
[decidable_pred (λ (_x : α), _x ∈ s)]
[decidable_pred (λ (_x : α), _x ∈ t)] :
decidable_pred (λ (_x : α), _x ∈ s * t)
Equations
- set.decidable_mem_mul = λ (_x : α), decidable_of_iff (∃ (x y : α), x ∈ s ∧ y ∈ t ∧ x * y = _x) _
@[protected, instance]
def
set.decidable_mem_pow
{α : Type u_2}
{s : set α}
[monoid α]
[fintype α]
[decidable_eq α]
[decidable_pred (λ (_x : α), _x ∈ s)]
(n : ℕ) :
decidable_pred (λ (_x : α), _x ∈ s ^ n)
Equations
- set.decidable_mem_pow n = nat.rec (set.decidable_mem_pow._proof_1.mpr (set.decidable_mem_pow._proof_2.mpr (λ (a : α), _inst_3 a 1))) (λ (n : ℕ) (ih : decidable_pred (λ (_x : α), _x ∈ s ^ n)), let _inst : decidable_pred (λ (_x : α), _x ∈ s ^ n) := ih in _.mpr (λ (a : α), set.decidable_mem_mul a)) n
theorem
set.subset_add_left
{α : Type u_2}
[add_zero_class α]
(s : set α)
{t : set α}
(ht : 0 ∈ t) :
theorem
set.subset_add_right
{α : Type u_2}
[add_zero_class α]
{s : set α}
(t : set α)
(hs : 0 ∈ s) :
theorem
set.subset_mul_right
{α : Type u_2}
[mul_one_class α]
{s : set α}
(t : set α)
(hs : 1 ∈ s) :
@[simp]
singleton is a monoid hom.
Equations
- set.singleton_hom = {to_fun := singleton set.has_singleton, map_one' := _, map_mul' := _}
def
set.fintype_add
{α : Type u_2}
[has_add α]
[decidable_eq α]
(s t : set α)
[hs : fintype ↥s]
[ht : fintype ↥t] :
addition preserves finiteness
Equations
- s.fintype_add t = set.fintype_image2 (λ (a b : α), a + b) s t
def
set.fintype_mul
{α : Type u_2}
[has_mul α]
[decidable_eq α]
(s t : set α)
[hs : fintype ↥s]
[ht : fintype ↥t] :
multiplication preserves finiteness
Equations
- s.fintype_mul t = set.fintype_image2 (λ (a b : α), a * b) s t
theorem
set.mem_finset_sum
{α : Type u_2}
{ι : Type u_5}
[add_comm_monoid α]
(t : finset ι)
(f : ι → set α)
(a : α) :
The n-ary version of set.mem_add.
theorem
set.mem_finset_prod
{α : Type u_2}
{ι : Type u_5}
[comm_monoid α]
(t : finset ι)
(f : ι → set α)
(a : α) :
The n-ary version of set.mem_mul.
theorem
set.mem_fintype_prod
{α : Type u_2}
{ι : Type u_5}
[comm_monoid α]
[fintype ι]
(f : ι → set α)
(a : α) :
A version of set.mem_finset_prod with a simpler RHS for products over a fintype.
theorem
set.mem_fintype_sum
{α : Type u_2}
{ι : Type u_5}
[add_comm_monoid α]
[fintype ι]
(f : ι → set α)
(a : α) :
A version of set.mem_finset_sum with a simpler RHS for sums over a fintype.
theorem
set.finset_prod_mem_finset_prod
{α : Type u_2}
{ι : Type u_5}
[comm_monoid α]
(t : finset ι)
(f : ι → set α)
(g : ι → α)
(hg : ∀ (i : ι), i ∈ t → g i ∈ f i) :
∏ (i : ι) in t, g i ∈ ∏ (i : ι) in t, f i
The n-ary version of set.mul_mem_mul.
theorem
set.finset_sum_mem_finset_sum
{α : Type u_2}
{ι : Type u_5}
[add_comm_monoid α]
(t : finset ι)
(f : ι → set α)
(g : ι → α)
(hg : ∀ (i : ι), i ∈ t → g i ∈ f i) :
∑ (i : ι) in t, g i ∈ ∑ (i : ι) in t, f i
The n-ary version of set.add_mem_add.
theorem
set.finset_prod_subset_finset_prod
{α : Type u_2}
{ι : Type u_5}
[comm_monoid α]
(t : finset ι)
(f₁ f₂ : ι → set α)
(hf : ∀ {i : ι}, i ∈ t → f₁ i ⊆ f₂ i) :
∏ (i : ι) in t, f₁ i ⊆ ∏ (i : ι) in t, f₂ i
The n-ary version of set.mul_subset_mul.
theorem
set.finset_sum_subset_finset_sum
{α : Type u_2}
{ι : Type u_5}
[add_comm_monoid α]
(t : finset ι)
(f₁ f₂ : ι → set α)
(hf : ∀ {i : ι}, i ∈ t → f₁ i ⊆ f₂ i) :
∑ (i : ι) in t, f₁ i ⊆ ∑ (i : ι) in t, f₂ i
The n-ary version of set.add_subset_add.
theorem
set.finset_prod_singleton
{M : Type u_1}
{ι : Type u_2}
[comm_monoid M]
(s : finset ι)
(I : ι → M) :
∏ (i : ι) in s, {I i} = {∏ (i : ι) in s, I i}
theorem
set.finset_sum_singleton
{M : Type u_1}
{ι : Type u_2}
[add_comm_monoid M]
(s : finset ι)
(I : ι → M) :
∑ (i : ι) in s, {I i} = {∑ (i : ι) in s, I i}
TODO: define decidable_mem_finset_prod and decidable_mem_finset_sum.
Set negation/inversion #
@[protected, instance]
The set (-s : set α) is defined as {x | -x ∈ s} in locale pointwise.
It is equal to {-x | x ∈ s}, see set.image_neg.
Equations
@[protected, instance]
The set (s⁻¹ : set α) is defined as {x | x⁻¹ ∈ s} in locale pointwise.
It is equal to {x⁻¹ | x ∈ s}, see set.image_inv.
Equations
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[protected, simp, instance]
Equations
- set.has_involutive_neg = {neg := has_neg.neg set.has_neg, neg_neg := _}
@[protected, simp, instance]
Equations
- set.has_involutive_inv = {inv := has_inv.inv set.has_inv, inv_inv := _}
@[simp]
@[simp]
theorem
set.image_op_inv
{α : Type u_2}
[has_involutive_inv α]
{s : set α} :
mul_opposite.op '' s⁻¹ = (mul_opposite.op '' s)⁻¹
@[protected]
Set multiplication/division #
@[protected, instance]
The set (s / t : set α) is defined as {x / y | x ∈ s, y ∈ t} in locale pointwise.
Equations
@[protected, instance]
The set (s - t : set α) is defined as {x - y | x ∈ s, y ∈ t} in locale
pointwise.
Equations
@[simp]
theorem
set.image2_sub
{α : Type u_2}
{s t : set α}
[has_sub α] :
set.image2 has_sub.sub s t = s - t
@[simp]
theorem
set.image2_div
{α : Type u_2}
{s t : set α}
[has_div α] :
set.image2 has_div.div s t = s / t
@[simp]
theorem
set.singleton_div
{α : Type u_2}
{t : set α}
{a : α}
[has_div α] :
{a} / t = has_div.div a '' t
@[simp]
theorem
set.singleton_sub
{α : Type u_2}
{t : set α}
{a : α}
[has_sub α] :
{a} - t = has_sub.sub a '' t
@[protected, instance]
Repeated pointwise addition (not the same as pointwise repeated addition!) of a finset.
Equations
@[protected, instance]
Repeated pointwise addition/subtraction (not the same as pointwise repeated
addition/subtraction!) of a set.
Equations
@[protected, instance]
Repeated pointwise multiplication/division (not the same as pointwise repeated
multiplication/division!) of a set.
@[protected, instance]
s / t = s * t⁻¹ for all s t : set α if a / b = a * b⁻¹ for all a b : α.
Equations
- set.div_inv_monoid = {mul := monoid.mul set.monoid, mul_assoc := _, one := monoid.one set.monoid, one_mul := _, mul_one := _, npow := monoid.npow set.monoid, npow_zero' := _, npow_succ' := _, inv := has_inv.inv set.has_inv, div := has_div.div set.has_div, div_eq_mul_inv := _, zpow := zpow_rec {inv := has_inv.inv set.has_inv}, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _}
@[protected, instance]
s - t = s + -t for all s t : set α if a - b = a + -b for all a b : α.
Equations
- set.sub_neg_add_monoid = {add := add_monoid.add set.add_monoid, add_assoc := _, zero := add_monoid.zero set.add_monoid, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul set.add_monoid, nsmul_zero' := _, nsmul_succ' := _, neg := has_neg.neg set.has_neg, sub := has_sub.sub set.has_sub, sub_eq_add_neg := _, zsmul := zsmul_rec {neg := has_neg.neg set.has_neg}, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _}
@[protected, instance]
s / t = s * t⁻¹ for all s t : set α if a / b = a * b⁻¹ for all a b : α.
Equations
- set.div_inv_monoid' = {mul := monoid.mul set.monoid, mul_assoc := _, one := monoid.one set.monoid, one_mul := _, mul_one := _, npow := monoid.npow set.monoid, npow_zero' := _, npow_succ' := _, inv := has_inv.inv set.has_inv, div := has_div.div set.has_div, div_eq_mul_inv := _, zpow := zpow_rec {inv := has_inv.inv set.has_inv}, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _}
Translation/scaling of sets #
@[protected, instance]
The translation of a set (x +ᵥ s : set β) by a scalar x ∶ α is
defined as {x +ᵥ y | y ∈ s} in locale pointwise.
Equations
- set.has_vadd_set = {vadd := λ (a : α), set.image (has_vadd.vadd a)}
@[protected, instance]
The scaling of a set (x • s : set β) by a scalar x ∶ α is defined as {x • y | y ∈ s}
in locale pointwise.
Equations
- set.has_scalar_set = {smul := λ (a : α), set.image (has_scalar.smul a)}
@[simp]
theorem
set.image2_smul
{α : Type u_2}
{β : Type u_3}
[has_scalar α β]
{s : set α}
{t : set β} :
set.image2 has_scalar.smul s t = s • t
@[simp]
theorem
set.image2_vadd
{α : Type u_2}
{β : Type u_3}
[has_vadd α β]
{s : set α}
{t : set β} :
set.image2 has_vadd.vadd s t = s +ᵥ t
theorem
set.smul_mem_smul
{α : Type u_2}
{β : Type u_3}
[has_scalar α β]
{s : set α}
{t : set β}
{a : α}
{b : β}
(ha : a ∈ s)
(hb : b ∈ t) :
theorem
set.smul_subset_smul
{α : Type u_2}
{β : Type u_3}
[has_scalar α β]
{s₁ s₂ : set α}
{t₁ t₂ : set β}
(hs : s₁ ⊆ s₂)
(ht : t₁ ⊆ t₂) :
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
theorem
set.singleton_smul_singleton
{α : Type u_2}
{β : Type u_3}
[has_scalar α β]
{a : α}
{b : β} :
theorem
set.smul_subset_smul_left
{α : Type u_2}
{β : Type u_3}
[has_scalar α β]
{s : set α}
{t₁ t₂ : set β}
(h : t₁ ⊆ t₂) :
theorem
set.smul_subset_smul_right
{α : Type u_2}
{β : Type u_3}
[has_scalar α β]
{s₁ s₂ : set α}
{t : set β}
(h : s₁ ⊆ s₂) :
theorem
set.Union_smul_left_image
{α : Type u_2}
{β : Type u_3}
[has_scalar α β]
{s : set α}
{t : set β} :
theorem
set.Union_smul_right_image
{α : Type u_2}
{β : Type u_3}
[has_scalar α β]
{s : set α}
{t : set β} :
theorem
set.Union_smul
{α : Type u_2}
{β : Type u_3}
{ι : Sort u_5}
[has_scalar α β]
(s : ι → set α)
(t : set β) :
theorem
set.smul_Union
{α : Type u_2}
{β : Type u_3}
{ι : Sort u_5}
[has_scalar α β]
(s : set α)
(t : ι → set β) :
theorem
set.Union₂_smul
{α : Type u_2}
{β : Type u_3}
{ι : Sort u_5}
{κ : ι → Sort u_6}
[has_scalar α β]
(s : Π (i : ι), κ i → set α)
(t : set β) :
theorem
set.smul_Union₂
{α : Type u_2}
{β : Type u_3}
{ι : Sort u_5}
{κ : ι → Sort u_6}
[has_scalar α β]
(s : set α)
(t : Π (i : ι), κ i → set β) :
theorem
set.Inter_smul_subset
{α : Type u_2}
{β : Type u_3}
{ι : Sort u_5}
[has_scalar α β]
(s : ι → set α)
(t : set β) :
theorem
set.smul_Inter_subset
{α : Type u_2}
{β : Type u_3}
{ι : Sort u_5}
[has_scalar α β]
(s : set α)
(t : ι → set β) :
theorem
set.Inter₂_smul_subset
{α : Type u_2}
{β : Type u_3}
{ι : Sort u_5}
{κ : ι → Sort u_6}
[has_scalar α β]
(s : Π (i : ι), κ i → set α)
(t : set β) :
theorem
set.smul_Inter₂_subset
{α : Type u_2}
{β : Type u_3}
{ι : Sort u_5}
{κ : ι → Sort u_6}
[has_scalar α β]
(s : set α)
(t : Π (i : ι), κ i → set β) :
@[simp]
theorem
set.smul_mem_smul_set
{α : Type u_2}
{β : Type u_3}
[has_scalar α β]
{t : set β}
{a : α}
{y : β}
(hy : y ∈ t) :
theorem
set.mem_smul_of_mem
{α : Type u_2}
{β : Type u_3}
[has_scalar α β]
{t : set β}
{a : α}
{b : β}
{s : set α}
(ha : a ∈ s)
(hb : b ∈ t) :
@[simp]
@[simp]
theorem
set.smul_set_mono
{α : Type u_2}
{β : Type u_3}
[has_scalar α β]
{s t : set β}
{a : α}
(h : s ⊆ t) :
theorem
set.smul_set_inter_subset
{α : Type u_2}
{β : Type u_3}
[has_scalar α β]
{t₁ t₂ : set β}
{a : α} :
theorem
set.smul_set_Union
{α : Type u_2}
{β : Type u_3}
{ι : Sort u_5}
[has_scalar α β]
(a : α)
(s : ι → set β) :
theorem
set.smul_set_Union₂
{α : Type u_2}
{β : Type u_3}
{ι : Sort u_5}
{κ : ι → Sort u_6}
[has_scalar α β]
(a : α)
(s : Π (i : ι), κ i → set β) :
theorem
set.smul_set_Inter_subset
{α : Type u_2}
{β : Type u_3}
{ι : Sort u_5}
[has_scalar α β]
(a : α)
(t : ι → set β) :
theorem
set.smul_set_Inter₂_subset
{α : Type u_2}
{β : Type u_3}
{ι : Sort u_5}
{κ : ι → Sort u_6}
[has_scalar α β]
(a : α)
(t : Π (i : ι), κ i → set β) :
theorem
set.smul_set_inter₀
{α : Type u_2}
{β : Type u_3}
{a : α}
[group_with_zero α]
[mul_action α β]
{s t : set β}
(ha : a ≠ 0) :
@[simp]
@[simp]
@[simp]
theorem
set.vadd_univ
{α : Type u_2}
{β : Type u_3}
[add_group α]
[add_action α β]
{s : set α}
(hs : s.nonempty) :
@[simp]
theorem
set.smul_univ
{α : Type u_2}
{β : Type u_3}
[group α]
[mul_action α β]
{s : set α}
(hs : s.nonempty) :
@[protected, instance]
def
set.vadd_comm_class_set
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[has_vadd α γ]
[has_vadd β γ]
[vadd_comm_class α β γ] :
vadd_comm_class α (set β) (set γ)
@[protected, instance]
def
set.smul_comm_class_set
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[has_scalar α γ]
[has_scalar β γ]
[smul_comm_class α β γ] :
smul_comm_class α (set β) (set γ)
@[protected, instance]
def
set.vadd_comm_class_set'
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[has_vadd α γ]
[has_vadd β γ]
[vadd_comm_class α β γ] :
vadd_comm_class (set α) β (set γ)
@[protected, instance]
def
set.smul_comm_class_set'
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[has_scalar α γ]
[has_scalar β γ]
[smul_comm_class α β γ] :
smul_comm_class (set α) β (set γ)
@[protected, instance]
def
set.vadd_comm_class
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[has_vadd α γ]
[has_vadd β γ]
[vadd_comm_class α β γ] :
vadd_comm_class (set α) (set β) (set γ)
@[protected, instance]
def
set.smul_comm_class
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[has_scalar α γ]
[has_scalar β γ]
[smul_comm_class α β γ] :
smul_comm_class (set α) (set β) (set γ)
@[protected, instance]
def
set.is_scalar_tower
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[has_scalar α β]
[has_scalar α γ]
[has_scalar β γ]
[is_scalar_tower α β γ] :
is_scalar_tower α β (set γ)
@[protected, instance]
def
set.is_scalar_tower'
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[has_scalar α β]
[has_scalar α γ]
[has_scalar β γ]
[is_scalar_tower α β γ] :
is_scalar_tower α (set β) (set γ)
@[protected, instance]
def
set.is_scalar_tower''
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[has_scalar α β]
[has_scalar α γ]
[has_scalar β γ]
[is_scalar_tower α β γ] :
is_scalar_tower (set α) (set β) (set γ)
@[protected, instance]
def
set.is_central_scalar
{α : Type u_2}
{β : Type u_3}
[has_scalar α β]
[has_scalar αᵐᵒᵖ β]
[is_central_scalar α β] :
is_central_scalar α (set β)
@[protected, instance]
def
set.mul_action
{α : Type u_2}
{β : Type u_3}
[monoid α]
[mul_action α β] :
mul_action (set α) (set β)
A multiplicative action of a monoid α on a type β gives a multiplicative action of set α
on set β.
Equations
- set.mul_action = {to_has_scalar := set.has_scalar mul_action.to_has_scalar, one_smul := _, mul_smul := _}
@[protected, instance]
def
set.add_action
{α : Type u_2}
{β : Type u_3}
[add_monoid α]
[add_action α β] :
add_action (set α) (set β)
An additive action of an additive monoid α on a type β gives an additive action
of set α on set β
Equations
- set.add_action = {to_has_vadd := set.has_vadd add_action.to_has_vadd, zero_vadd := _, add_vadd := _}
@[protected, instance]
def
set.add_action_set
{α : Type u_2}
{β : Type u_3}
[add_monoid α]
[add_action α β] :
add_action α (set β)
An additive action of an additive monoid on a type β gives an additive action
on set β.
Equations
- set.add_action_set = {to_has_vadd := set.has_vadd_set add_action.to_has_vadd, zero_vadd := _, add_vadd := _}
@[protected, instance]
def
set.mul_action_set
{α : Type u_2}
{β : Type u_3}
[monoid α]
[mul_action α β] :
mul_action α (set β)
A multiplicative action of a monoid on a type β gives a multiplicative action on set β.
Equations
@[protected, instance]
def
set.distrib_mul_action_set
{α : Type u_2}
{β : Type u_3}
[monoid α]
[add_monoid β]
[distrib_mul_action α β] :
distrib_mul_action α (set β)
A distributive multiplicative action of a monoid on an additive monoid β gives a distributive
multiplicative action on set β.
Equations
@[protected, instance]
def
set.mul_distrib_mul_action_set
{α : Type u_2}
{β : Type u_3}
[monoid α]
[monoid β]
[mul_distrib_mul_action α β] :
mul_distrib_mul_action α (set β)
A multiplicative action of a monoid on a monoid β gives a multiplicative action on set β.
Equations
@[protected, instance]
Equations
@[simp]
theorem
set.image2_vsub
{α : Type u_2}
{β : Type u_3}
[has_vsub α β]
{s t : set β} :
set.image2 has_vsub.vsub s t = s -ᵥ t
@[simp]
theorem
set.singleton_vsub
{α : Type u_2}
{β : Type u_3}
[has_vsub α β]
(t : set β)
(b : β) :
{b} -ᵥ t = has_vsub.vsub b '' t
theorem
set.Union_vsub_left_image
{α : Type u_2}
{β : Type u_3}
[has_vsub α β]
{s t : set β} :
(⋃ (a : β) (H : a ∈ s), has_vsub.vsub a '' t) = s -ᵥ t
@[protected, instance]
@[protected, instance]
An alias for set α, which has a semiring structure given by ∪ as "addition" and pointwise
multiplication * as "multiplication".
Equations
- set.set_semiring α = set α
@[protected, instance]
@[protected]
The identity function set_semiring α → set α.
@[protected, simp]
@[simp]
@[simp]
@[protected, instance]
Equations
- set.set_semiring.add_comm_monoid = {add := λ (s t : set.set_semiring α), s ∪ t, add_assoc := _, zero := ∅, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul._default ∅ (λ (s t : set.set_semiring α), s ∪ t) set.empty_union set.union_empty, nsmul_zero' := _, nsmul_succ' := _, add_comm := _}
@[protected, instance]
Equations
- set.set_semiring.non_unital_non_assoc_semiring = {add := add_comm_monoid.add set.set_semiring.add_comm_monoid, add_assoc := _, zero := add_comm_monoid.zero set.set_semiring.add_comm_monoid, zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul set.set_semiring.add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := has_mul.mul set.has_mul, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _}
@[protected, instance]
Equations
- set.set_semiring.non_assoc_semiring = {add := non_unital_non_assoc_semiring.add set.set_semiring.non_unital_non_assoc_semiring, add_assoc := _, zero := non_unital_non_assoc_semiring.zero set.set_semiring.non_unital_non_assoc_semiring, zero_add := _, add_zero := _, nsmul := non_unital_non_assoc_semiring.nsmul set.set_semiring.non_unital_non_assoc_semiring, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := non_unital_non_assoc_semiring.mul set.set_semiring.non_unital_non_assoc_semiring, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, one := mul_one_class.one set.mul_one_class, one_mul := _, mul_one := _}
@[protected, instance]
Equations
- set.set_semiring.non_unital_semiring = {add := non_unital_non_assoc_semiring.add set.set_semiring.non_unital_non_assoc_semiring, add_assoc := _, zero := non_unital_non_assoc_semiring.zero set.set_semiring.non_unital_non_assoc_semiring, zero_add := _, add_zero := _, nsmul := non_unital_non_assoc_semiring.nsmul set.set_semiring.non_unital_non_assoc_semiring, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := non_unital_non_assoc_semiring.mul set.set_semiring.non_unital_non_assoc_semiring, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _}
@[protected, instance]
Equations
- set.set_semiring.semiring = {add := non_assoc_semiring.add set.set_semiring.non_assoc_semiring, add_assoc := _, zero := non_assoc_semiring.zero set.set_semiring.non_assoc_semiring, zero_add := _, add_zero := _, nsmul := non_assoc_semiring.nsmul set.set_semiring.non_assoc_semiring, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := non_assoc_semiring.mul set.set_semiring.non_assoc_semiring, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := non_assoc_semiring.one set.set_semiring.non_assoc_semiring, one_mul := _, mul_one := _, npow := monoid_with_zero.npow._default non_assoc_semiring.one non_assoc_semiring.mul set.set_semiring.semiring._proof_14 set.set_semiring.semiring._proof_15, npow_zero' := _, npow_succ' := _}
@[protected, instance]
Equations
- set.set_semiring.comm_semiring = {add := semiring.add set.set_semiring.semiring, add_assoc := _, zero := semiring.zero set.set_semiring.semiring, zero_add := _, add_zero := _, nsmul := semiring.nsmul set.set_semiring.semiring, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := comm_monoid.mul set.comm_monoid, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := comm_monoid.one set.comm_monoid, one_mul := _, mul_one := _, npow := comm_monoid.npow set.comm_monoid, npow_zero' := _, npow_succ' := _, mul_comm := _}
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
The image of a set under a multiplicative homomorphism is a ring homomorphism with respect to the pointwise operations on sets.
@[protected, instance]
Equations
- set.set_semiring.canonically_ordered_comm_semiring = {add := comm_semiring.add infer_instance, add_assoc := _, zero := comm_semiring.zero infer_instance, zero_add := _, add_zero := _, nsmul := comm_semiring.nsmul infer_instance, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, le := partial_order.le infer_instance, lt := partial_order.lt infer_instance, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, bot := order_bot.bot infer_instance, bot_le := _, le_iff_exists_add := _, mul := comm_semiring.mul infer_instance, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := comm_semiring.one infer_instance, one_mul := _, mul_one := _, npow := comm_semiring.npow infer_instance, npow_zero' := _, npow_succ' := _, mul_comm := _, eq_zero_or_eq_zero_of_mul_eq_zero := _}
theorem
zero_smul_set
{α : Type u_2}
{β : Type u_3}
[has_zero α]
[has_zero β]
[smul_with_zero α β]
{s : set β}
(h : s.nonempty) :
A nonempty set is scaled by zero to the singleton set containing 0.
theorem
zero_smul_subset
{α : Type u_2}
{β : Type u_3}
[has_zero α]
[has_zero β]
[smul_with_zero α β]
(s : set β) :
theorem
subsingleton_zero_smul_set
{α : Type u_2}
{β : Type u_3}
[has_zero α]
[has_zero β]
[smul_with_zero α β]
(s : set β) :
(0 • s).subsingleton
theorem
zero_mem_smul_set
{α : Type u_2}
{β : Type u_3}
[has_zero α]
[has_zero β]
[smul_with_zero α β]
{t : set β}
{a : α}
(h : 0 ∈ t) :
theorem
zero_mem_smul_set_iff
{α : Type u_2}
{β : Type u_3}
[has_zero α]
[has_zero β]
[smul_with_zero α β]
[no_zero_smul_divisors α β]
{t : set β}
{a : α}
(ha : a ≠ 0) :
theorem
smul_add_set
{α : Type u_2}
{β : Type u_3}
[monoid α]
[add_monoid β]
[distrib_mul_action α β]
(c : α)
(s t : set β) :
@[simp]
theorem
smul_mem_smul_set_iff
{α : Type u_2}
{β : Type u_3}
[group α]
[mul_action α β]
{A : set β}
{a : α}
{x : β} :
@[simp]
theorem
vadd_mem_vadd_set_iff
{α : Type u_2}
{β : Type u_3}
[add_group α]
[add_action α β]
{A : set β}
{a : α}
{x : β} :
theorem
preimage_smul
{α : Type u_2}
{β : Type u_3}
[group α]
[mul_action α β]
(a : α)
(t : set β) :
theorem
preimage_vadd
{α : Type u_2}
{β : Type u_3}
[add_group α]
[add_action α β]
(a : α)
(t : set β) :
theorem
preimage_smul_inv
{α : Type u_2}
{β : Type u_3}
[group α]
[mul_action α β]
(a : α)
(t : set β) :
theorem
preimage_vadd_neg
{α : Type u_2}
{β : Type u_3}
[add_group α]
[add_action α β]
(a : α)
(t : set β) :
@[simp]
theorem
set_smul_subset_set_smul_iff
{α : Type u_2}
{β : Type u_3}
[group α]
[mul_action α β]
{A B : set β}
{a : α} :
@[simp]
theorem
set_vadd_subset_set_vadd_iff
{α : Type u_2}
{β : Type u_3}
[add_group α]
[add_action α β]
{A B : set β}
{a : α} :
@[simp]
theorem
smul_mem_smul_set_iff₀
{α : Type u_2}
{β : Type u_3}
[group_with_zero α]
[mul_action α β]
{a : α}
(ha : a ≠ 0)
(A : set β)
(x : β) :
theorem
mem_smul_set_iff_inv_smul_mem₀
{α : Type u_2}
{β : Type u_3}
[group_with_zero α]
[mul_action α β]
{a : α}
(ha : a ≠ 0)
(A : set β)
(x : β) :
theorem
mem_inv_smul_set_iff₀
{α : Type u_2}
{β : Type u_3}
[group_with_zero α]
[mul_action α β]
{a : α}
(ha : a ≠ 0)
(A : set β)
(x : β) :
theorem
preimage_smul₀
{α : Type u_2}
{β : Type u_3}
[group_with_zero α]
[mul_action α β]
{a : α}
(ha : a ≠ 0)
(t : set β) :
theorem
preimage_smul_inv₀
{α : Type u_2}
{β : Type u_3}
[group_with_zero α]
[mul_action α β]
{a : α}
(ha : a ≠ 0)
(t : set β) :
@[simp]
theorem
set_smul_subset_set_smul_iff₀
{α : Type u_2}
{β : Type u_3}
[group_with_zero α]
[mul_action α β]
{a : α}
(ha : a ≠ 0)
{A B : set β} :
theorem
set_smul_subset_iff₀
{α : Type u_2}
{β : Type u_3}
[group_with_zero α]
[mul_action α β]
{a : α}
(ha : a ≠ 0)
{A B : set β} :
theorem
subset_set_smul_iff₀
{α : Type u_2}
{β : Type u_3}
[group_with_zero α]
[mul_action α β]
{a : α}
(ha : a ≠ 0)
{A B : set β} :
theorem
smul_univ₀
{α : Type u_2}
{β : Type u_3}
[group_with_zero α]
[mul_action α β]
{s : set α}
(hs : ¬s ⊆ 0) :
theorem
smul_set_univ₀
{α : Type u_2}
{β : Type u_3}
[group_with_zero α]
[mul_action α β]
{a : α}
(ha : a ≠ 0) :
Some lemmas about pointwise multiplication and submonoids. Ideally we put these in
group_theory.submonoid.basic, but currently we cannot because that file is imported by this.
theorem
add_submonoid.add_subset
{M : Type u_5}
[add_monoid M]
{s t : set M}
{S : add_submonoid M}
(hs : s ⊆ ↑S)
(ht : t ⊆ ↑S) :
theorem
add_submonoid.add_subset_closure
{M : Type u_5}
[add_monoid M]
{s t u : set M}
(hs : s ⊆ u)
(ht : t ⊆ u) :
s + t ⊆ ↑(add_submonoid.closure u)
theorem
submonoid.mul_subset_closure
{M : Type u_5}
[monoid M]
{s t u : set M}
(hs : s ⊆ u)
(ht : t ⊆ u) :
s * t ⊆ ↑(submonoid.closure u)
theorem
submonoid.closure_mul_le
{M : Type u_5}
[monoid M]
(S T : set M) :
submonoid.closure (S * T) ≤ submonoid.closure S ⊔ submonoid.closure T
theorem
submonoid.pow_smul_mem_closure_smul
{M : Type u_5}
[monoid M]
{N : Type u_1}
[comm_monoid N]
[mul_action M N]
[is_scalar_tower M N N]
(r : M)
(s : set N)
{x : N}
(hx : x ∈ submonoid.closure s) :
theorem
group.card_pow_eq_card_pow_card_univ
{G : Type u_5}
[group G]
[fintype G]
(S : set G)
[Π (k : ℕ), decidable_pred (λ (_x : G), _x ∈ S ^ k)]
(k : ℕ) :
fintype.card G ≤ k → fintype.card ↥(S ^ k) = fintype.card ↥(S ^ fintype.card G)
theorem
add_group.card_nsmul_eq_card_nsmul_card_univ
{G : Type u_5}
[add_group G]
[fintype G]
(S : set G)
[Π (k : ℕ), decidable_pred (λ (_x : G), _x ∈ k • S)]
(k : ℕ) :
fintype.card G ≤ k → fintype.card ↥(k • S) = fintype.card ↥(fintype.card G • S)