mathlib documentation

data.set.pointwise

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 all x * y where x ∈ s and y ∈ t.
s + t: Addition, set of all x + y where x ∈ s and y ∈ t.
s⁻¹: Inversion, set of all x⁻¹ where x ∈ s.
-s: Negation, set of all -x where x ∈ s.
s / t: Division, set of all x / y where x ∈ s and y ∈ t.
s - t: Subtraction, set of all x - y where x ∈ s and y ∈ t.
s • t: Scalar multiplication, set of all x • y where x ∈ s and y ∈ t.
s +ᵥ t: Scalar addition, set of all x +ᵥ y where x ∈ s and y ∈ t.
s -ᵥ t: Scalar subtraction, set of all x -ᵥ y where x ∈ s and y ∈ t.
a • s: Scaling, set of all a • x where x ∈ s.
a +ᵥ s: Translation, set of all a +ᵥ x where x ∈ 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}. See note [pointwise nat action].

Appropriate definitions and results are also transported to the additive theory via to_additive.

Definitions for Hahn series #

set.add_antidiagonal s t a, set.mul_antidiagonal s t a: Sets of pairs of elements of s and t that add/multiply to a.
finset.add_antidiagonal, finset.mul_antidiagonal: Finset versions of the above when s and t are well-founded.

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 of simp.

Tags #

set multiplication, set addition, pointwise addition, pointwise multiplication, pointwise subtraction

def library_note.pointwise nat action :

Pointwise monoids (set, finset, filter) have derived pointwise actions of the form has_smul α β → has_smul α (set β). When α is ℕ or ℤ, this action conflicts with the nat or int action coming from set β being a monoid or div_inv_monoid. For example, 2 • {a, b} can both be {2 • a, 2 • b} (pointwise action, pointwise repeated addition, set.has_smul_set) and {a + a, a + b, b + a, b + b} (nat or int action, repeated pointwise addition, set.has_nsmul).

Because the pointwise action can easily be spelled out in such cases, we give higher priority to the nat and int actions.

`0`/`1` as sets #

@[protected]

def set.has_one {α : Type u_2} [has_one α] :

has_one (set α)

The set 1 : set α is defined as {1} in locale pointwise.

Equations

set.has_one = {one := {1}}

@[protected]

def set.has_zero {α : Type u_2} [has_zero α] :

has_zero (set α)

The set 0 : set α is defined as {0} in locale pointwise.

Equations

set.has_zero = {zero := {0}}

theorem set.singleton_one {α : Type u_2} [has_one α] :

{1} = 1

theorem set.singleton_zero {α : Type u_2} [has_zero α] :

{0} = 0

@[simp]

theorem set.mem_one {α : Type u_2} [has_one α] {a : α} :

a ∈ 1 ↔ a = 1

@[simp]

theorem set.mem_zero {α : Type u_2} [has_zero α] {a : α} :

a ∈ 0 ↔ a = 0

theorem set.zero_mem_zero {α : Type u_2} [has_zero α] :

0 ∈ 0

theorem set.one_mem_one {α : Type u_2} [has_one α] :

1 ∈ 1

@[simp]

theorem set.zero_subset {α : Type u_2} [has_zero α] {s : set α} :

0 ⊆ s ↔ 0 ∈ s

@[simp]

theorem set.one_subset {α : Type u_2} [has_one α] {s : set α} :

1 ⊆ s ↔ 1 ∈ s

theorem set.zero_nonempty {α : Type u_2} [has_zero α] :

theorem set.one_nonempty {α : Type u_2} [has_one α] :

@[simp]

theorem set.image_zero {α : Type u_2} {β : Type u_3} [has_zero α] {f : α → β} :

f '' 0 = {f 0}

@[simp]

theorem set.image_one {α : Type u_2} {β : Type u_3} [has_one α] {f : α → β} :

f '' 1 = {f 1}

theorem set.subset_zero_iff_eq {α : Type u_2} [has_zero α] {s : set α} :

s ⊆ 0 ↔ s = ∅ ∨ s = 0

theorem set.subset_one_iff_eq {α : Type u_2} [has_one α] {s : set α} :

s ⊆ 1 ↔ s = ∅ ∨ s = 1

theorem set.nonempty.subset_zero_iff {α : Type u_2} [has_zero α] {s : set α} (h : s.nonempty) :

s ⊆ 0 ↔ s = 0

theorem set.nonempty.subset_one_iff {α : Type u_2} [has_one α] {s : set α} (h : s.nonempty) :

s ⊆ 1 ↔ s = 1

def set.singleton_zero_hom {α : Type u_2} [has_zero α] :

zero_hom α (set α)

The singleton operation as a zero_hom.

Equations

set.singleton_zero_hom = {to_fun := has_singleton.singleton set.has_singleton, map_zero' := _}

def set.singleton_one_hom {α : Type u_2} [has_one α] :

one_hom α (set α)

The singleton operation as a one_hom.

Equations

set.singleton_one_hom = {to_fun := has_singleton.singleton set.has_singleton, map_one' := _}

@[simp]

theorem set.coe_singleton_zero_hom {α : Type u_2} [has_zero α] :

⇑set.singleton_zero_hom = has_singleton.singleton

@[simp]

theorem set.coe_singleton_one_hom {α : Type u_2} [has_one α] :

⇑set.singleton_one_hom = has_singleton.singleton

Set negation/inversion #

@[protected]

def set.has_neg {α : Type u_2} [has_neg α] :

has_neg (set α)

The pointwise negation of set -s is defined as {x | -x ∈ s} in locale pointwise. It is equal to {-x | x ∈ s}, see set.image_neg.

Equations

set.has_neg = {neg := set.preimage has_neg.neg}

@[protected]

def set.has_inv {α : Type u_2} [has_inv α] :

has_inv (set α)

The pointwise inversion of set s⁻¹ is defined as {x | x⁻¹ ∈ s} in locale pointwise. It i equal to {x⁻¹ | x ∈ s}, see set.image_inv.

Equations

set.has_inv = {inv := set.preimage has_inv.inv}

@[simp]

theorem set.mem_inv {α : Type u_2} [has_inv α] {s : set α} {a : α} :

a ∈ s⁻¹ ↔ a⁻¹ ∈ s

@[simp]

theorem set.mem_neg {α : Type u_2} [has_neg α] {s : set α} {a : α} :

a ∈ -s ↔ -a ∈ s

@[simp]

theorem set.inv_preimage {α : Type u_2} [has_inv α] {s : set α} :

has_inv.inv ⁻¹' s = s⁻¹

@[simp]

theorem set.neg_preimage {α : Type u_2} [has_neg α] {s : set α} :

has_neg.neg ⁻¹' s = -s

@[simp]

theorem set.neg_empty {α : Type u_2} [has_neg α] :

@[simp]

theorem set.inv_empty {α : Type u_2} [has_inv α] :

@[simp]

theorem set.neg_univ {α : Type u_2} [has_neg α] :

-set.univ = set.univ

@[simp]

theorem set.inv_univ {α : Type u_2} [has_inv α] :

set.univ ⁻¹ = set.univ

@[simp]

theorem set.inter_neg {α : Type u_2} [has_neg α] {s t : set α} :

-(s ∩ t) = -s ∩ -t

@[simp]

theorem set.inter_inv {α : Type u_2} [has_inv α] {s t : set α} :

(s ∩ t)⁻¹ = s⁻¹ ∩ t⁻¹

@[simp]

theorem set.union_neg {α : Type u_2} [has_neg α] {s t : set α} :

-(s ∪ t) = -s ∪ -t

@[simp]

theorem set.union_inv {α : Type u_2} [has_inv α] {s t : set α} :

(s ∪ t)⁻¹ = s⁻¹ ∪ t⁻¹

@[simp]

theorem set.Inter_inv {α : Type u_2} {ι : Sort u_5} [has_inv α] (s : ι → set α) :

(⋂ (i : ι), s i)⁻¹ = ⋂ (i : ι), (s i)⁻¹

@[simp]

theorem set.Inter_neg {α : Type u_2} {ι : Sort u_5} [has_neg α] (s : ι → set α) :

(-⋂ (i : ι), s i) = ⋂ (i : ι), -s i

@[simp]

theorem set.Union_inv {α : Type u_2} {ι : Sort u_5} [has_inv α] (s : ι → set α) :

(⋃ (i : ι), s i)⁻¹ = ⋃ (i : ι), (s i)⁻¹

@[simp]

theorem set.Union_neg {α : Type u_2} {ι : Sort u_5} [has_neg α] (s : ι → set α) :

(-⋃ (i : ι), s i) = ⋃ (i : ι), -s i

@[simp]

theorem set.compl_neg {α : Type u_2} [has_neg α] {s : set α} :

-sᶜ = (-s)ᶜ

@[simp]

theorem set.compl_inv {α : Type u_2} [has_inv α] {s : set α} :

sᶜ ⁻¹ = s⁻¹ ᶜ

theorem set.inv_mem_inv {α : Type u_2} [has_involutive_inv α] {s : set α} {a : α} :

a⁻¹ ∈ s⁻¹ ↔ a ∈ s

theorem set.neg_mem_neg {α : Type u_2} [has_involutive_neg α] {s : set α} {a : α} :

-a ∈ -s ↔ a ∈ s

@[simp]

theorem set.nonempty_neg {α : Type u_2} [has_involutive_neg α] {s : set α} :

(-s).nonempty ↔ s.nonempty

@[simp]

theorem set.nonempty_inv {α : Type u_2} [has_involutive_inv α] {s : set α} :

s⁻¹.nonempty ↔ s.nonempty

theorem set.nonempty.inv {α : Type u_2} [has_involutive_inv α] {s : set α} (h : s.nonempty) :

s⁻¹.nonempty

theorem set.nonempty.neg {α : Type u_2} [has_involutive_neg α] {s : set α} (h : s.nonempty) :

theorem set.finite.inv {α : Type u_2} [has_involutive_inv α] {s : set α} (hs : s.finite) :

theorem set.finite.neg {α : Type u_2} [has_involutive_neg α] {s : set α} (hs : s.finite) :

@[simp]

theorem set.image_inv {α : Type u_2} [has_involutive_inv α] {s : set α} :

has_inv.inv '' s = s⁻¹

@[simp]

theorem set.image_neg {α : Type u_2} [has_involutive_neg α] {s : set α} :

has_neg.neg '' s = -s

@[protected, simp, instance]

def set.has_involutive_neg {α : Type u_2} [has_involutive_neg α] :

has_involutive_neg (set α)

Equations

set.has_involutive_neg = {neg := has_neg.neg set.has_neg, neg_neg := _}

@[protected, simp, instance]

def set.has_involutive_inv {α : Type u_2} [has_involutive_inv α] :

has_involutive_inv (set α)

Equations

set.has_involutive_inv = {inv := has_inv.inv set.has_inv, inv_inv := _}

@[simp]

theorem set.neg_subset_neg {α : Type u_2} [has_involutive_neg α] {s t : set α} :

-s ⊆ -t ↔ s ⊆ t

@[simp]

theorem set.inv_subset_inv {α : Type u_2} [has_involutive_inv α] {s t : set α} :

s⁻¹ ⊆ t⁻¹ ↔ s ⊆ t

theorem set.inv_subset {α : Type u_2} [has_involutive_inv α] {s t : set α} :

s⁻¹ ⊆ t ↔ s ⊆ t⁻¹

theorem set.neg_subset {α : Type u_2} [has_involutive_neg α] {s t : set α} :

-s ⊆ t ↔ s ⊆ -t

@[simp]

theorem set.inv_singleton {α : Type u_2} [has_involutive_inv α] (a : α) :

{a}⁻¹ = {a⁻¹}

@[simp]

theorem set.neg_singleton {α : Type u_2} [has_involutive_neg α] (a : α) :

-{a} = {-a}

theorem set.inv_range {α : Type u_2} [has_involutive_inv α] {ι : Sort u_1} {f : ι → α} :

(set.range f)⁻¹ = set.range (λ (i : ι), (f i)⁻¹)

theorem set.neg_range {α : Type u_2} [has_involutive_neg α] {ι : Sort u_1} {f : ι → α} :

-set.range f = set.range (λ (i : ι), -f i)

theorem set.image_op_neg {α : Type u_2} [has_involutive_neg α] {s : set α} :

add_opposite.op '' -s = -add_opposite.op '' s

theorem set.image_op_inv {α : Type u_2} [has_involutive_inv α] {s : set α} :

mul_opposite.op '' s⁻¹ = (mul_opposite.op '' s)⁻¹

Set addition/multiplication #

@[protected]

def set.has_mul {α : Type u_2} [has_mul α] :

has_mul (set α)

The pointwise multiplication of sets s * t and t is defined as {x * y | x ∈ s, y ∈ t} in locale pointwise.

Equations

set.has_mul = {mul := set.image2 has_mul.mul}

@[protected]

def set.has_add {α : Type u_2} [has_add α] :

has_add (set α)

The pointwise addition of sets s + t is defined as {x + y | x ∈ s, y ∈ t} in locale pointwise.

Equations

set.has_add = {add := set.image2 has_add.add}

@[simp]

theorem set.image2_mul {α : Type u_2} [has_mul α] {s t : set α} :

set.image2 has_mul.mul s t = s * t

@[simp]

theorem set.image2_add {α : Type u_2} [has_add α] {s t : set α} :

set.image2 has_add.add s t = s + t

theorem set.mem_add {α : Type u_2} [has_add α] {s t : set α} {a : α} :

a ∈ s + t ↔ ∃ (x y : α), x ∈ s ∧ y ∈ t ∧ x + y = a

theorem set.mem_mul {α : Type u_2} [has_mul α] {s t : set α} {a : α} :

a ∈ s * t ↔ ∃ (x y : α), x ∈ s ∧ y ∈ t ∧ x * y = a

theorem set.mul_mem_mul {α : Type u_2} [has_mul α] {s t : set α} {a b : α} :

a ∈ s → b ∈ t → a * b ∈ s * t

theorem set.add_mem_add {α : Type u_2} [has_add α] {s t : set α} {a b : α} :

a ∈ s → b ∈ t → a + b ∈ s + t

theorem set.image_mul_prod {α : Type u_2} [has_mul α] {s t : set α} :

(λ (x : α × α), x.fst * x.snd) '' s ×ˢ t = s * t

theorem set.add_image_prod {α : Type u_2} [has_add α] {s t : set α} :

(λ (x : α × α), x.fst + x.snd) '' s ×ˢ t = s + t

@[simp]

theorem set.empty_mul {α : Type u_2} [has_mul α] {s : set α} :

@[simp]

theorem set.empty_add {α : Type u_2} [has_add α] {s : set α} :

@[simp]

theorem set.add_empty {α : Type u_2} [has_add α] {s : set α} :

@[simp]

theorem set.mul_empty {α : Type u_2} [has_mul α] {s : set α} :

@[simp]

theorem set.add_eq_empty {α : Type u_2} [has_add α] {s t : set α} :

s + t = ∅ ↔ s = ∅ ∨ t = ∅

@[simp]

theorem set.mul_eq_empty {α : Type u_2} [has_mul α] {s t : set α} :

s * t = ∅ ↔ s = ∅ ∨ t = ∅

@[simp]

theorem set.mul_nonempty {α : Type u_2} [has_mul α] {s t : set α} :

(s * t).nonempty ↔ s.nonempty ∧ t.nonempty

@[simp]

theorem set.add_nonempty {α : Type u_2} [has_add α] {s t : set α} :

(s + t).nonempty ↔ s.nonempty ∧ t.nonempty

theorem set.nonempty.add {α : Type u_2} [has_add α] {s t : set α} :

s.nonempty → t.nonempty → (s + t).nonempty

theorem set.nonempty.mul {α : Type u_2} [has_mul α] {s t : set α} :

s.nonempty → t.nonempty → (s * t).nonempty

theorem set.nonempty.of_add_left {α : Type u_2} [has_add α] {s t : set α} :

(s + t).nonempty → s.nonempty

theorem set.nonempty.of_mul_left {α : Type u_2} [has_mul α] {s t : set α} :

(s * t).nonempty → s.nonempty

theorem set.nonempty.of_add_right {α : Type u_2} [has_add α] {s t : set α} :

(s + t).nonempty → t.nonempty

theorem set.nonempty.of_mul_right {α : Type u_2} [has_mul α] {s t : set α} :

(s * t).nonempty → t.nonempty

@[simp]

theorem set.add_singleton {α : Type u_2} [has_add α] {s : set α} {b : α} :

s + {b} = (λ (_x : α), _x + b) '' s

@[simp]

theorem set.mul_singleton {α : Type u_2} [has_mul α] {s : set α} {b : α} :

s * {b} = (λ (_x : α), _x * b) '' s

@[simp]

theorem set.singleton_add {α : Type u_2} [has_add α] {t : set α} {a : α} :

{a} + t = has_add.add a '' t

@[simp]

theorem set.singleton_mul {α : Type u_2} [has_mul α] {t : set α} {a : α} :

{a} * t = has_mul.mul a '' t

@[simp]

theorem set.singleton_mul_singleton {α : Type u_2} [has_mul α] {a b : α} :

{a} * {b} = {a * b}

@[simp]

theorem set.singleton_add_singleton {α : Type u_2} [has_add α] {a b : α} :

{a} + {b} = {a + b}

theorem set.add_subset_add {α : Type u_2} [has_add α] {s₁ s₂ t₁ t₂ : set α} :

s₁ ⊆ t₁ → s₂ ⊆ t₂ → s₁ + s₂ ⊆ t₁ + t₂

theorem set.mul_subset_mul {α : Type u_2} [has_mul α] {s₁ s₂ t₁ t₂ : set α} :

s₁ ⊆ t₁ → s₂ ⊆ t₂ → s₁ * s₂ ⊆ t₁ * t₂

theorem set.add_subset_add_left {α : Type u_2} [has_add α] {s t₁ t₂ : set α} :

t₁ ⊆ t₂ → s + t₁ ⊆ s + t₂

theorem set.mul_subset_mul_left {α : Type u_2} [has_mul α] {s t₁ t₂ : set α} :

t₁ ⊆ t₂ → s * t₁ ⊆ s * t₂

theorem set.mul_subset_mul_right {α : Type u_2} [has_mul α] {s₁ s₂ t : set α} :

s₁ ⊆ s₂ → s₁ * t ⊆ s₂ * t

theorem set.add_subset_add_right {α : Type u_2} [has_add α] {s₁ s₂ t : set α} :

s₁ ⊆ s₂ → s₁ + t ⊆ s₂ + t

theorem set.mul_subset_iff {α : Type u_2} [has_mul α] {s t u : set α} :

s * t ⊆ u ↔ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ t → x * y ∈ u

theorem set.add_subset_iff {α : Type u_2} [has_add α] {s t u : set α} :

s + t ⊆ u ↔ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ t → x + y ∈ u

theorem set.union_mul {α : Type u_2} [has_mul α] {s₁ s₂ t : set α} :

(s₁ ∪ s₂) * t = s₁ * t ∪ s₂ * t

theorem set.union_add {α : Type u_2} [has_add α] {s₁ s₂ t : set α} :

s₁ ∪ s₂ + t = s₁ + t ∪ (s₂ + t)

theorem set.mul_union {α : Type u_2} [has_mul α] {s t₁ t₂ : set α} :

s * (t₁ ∪ t₂) = s * t₁ ∪ s * t₂

theorem set.add_union {α : Type u_2} [has_add α] {s t₁ t₂ : set α} :

s + (t₁ ∪ t₂) = s + t₁ ∪ (s + t₂)

theorem set.inter_add_subset {α : Type u_2} [has_add α] {s₁ s₂ t : set α} :

s₁ ∩ s₂ + t ⊆ (s₁ + t) ∩ (s₂ + t)

theorem set.inter_mul_subset {α : Type u_2} [has_mul α] {s₁ s₂ t : set α} :

s₁ ∩ s₂ * t ⊆ s₁ * t ∩ (s₂ * t)

theorem set.mul_inter_subset {α : Type u_2} [has_mul α] {s t₁ t₂ : set α} :

s * (t₁ ∩ t₂) ⊆ s * t₁ ∩ (s * t₂)

theorem set.add_inter_subset {α : Type u_2} [has_add α] {s t₁ t₂ : set α} :

s + t₁ ∩ t₂ ⊆ (s + t₁) ∩ (s + t₂)

theorem set.Union_mul_left_image {α : Type u_2} [has_mul α] {s t : set α} :

(⋃ (a : α) (H : a ∈ s), has_mul.mul a '' t) = s * t

theorem set.Union_add_left_image {α : Type u_2} [has_add α] {s t : set α} :

(⋃ (a : α) (H : a ∈ s), has_add.add a '' t) = s + t

theorem set.Union_mul_right_image {α : Type u_2} [has_mul α] {s t : set α} :

(⋃ (a : α) (H : a ∈ t), (λ (_x : α), _x * a) '' s) = s * t

theorem set.Union_add_right_image {α : Type u_2} [has_add α] {s t : set α} :

(⋃ (a : α) (H : a ∈ t), (λ (_x : α), _x + a) '' s) = s + t

theorem set.Union_add {α : Type u_2} {ι : Sort u_5} [has_add α] (s : ι → set α) (t : set α) :

(⋃ (i : ι), s i) + t = ⋃ (i : ι), s i + t

theorem set.Union_mul {α : Type u_2} {ι : Sort u_5} [has_mul α] (s : ι → set α) (t : set α) :

(⋃ (i : ι), s i) * t = ⋃ (i : ι), s i * t

theorem set.add_Union {α : Type u_2} {ι : Sort u_5} [has_add α] (s : set α) (t : ι → set α) :

(s + ⋃ (i : ι), t i) = ⋃ (i : ι), s + t i

theorem set.mul_Union {α : Type u_2} {ι : Sort u_5} [has_mul α] (s : set α) (t : ι → set α) :

(s * ⋃ (i : ι), t i) = ⋃ (i : ι), s * t i

theorem set.Union₂_add {α : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_6} [has_add α] (s : Π (i : ι), κ i → set α) (t : set α) :

(⋃ (i : ι) (j : κ i), s i j) + t = ⋃ (i : ι) (j : κ i), s i j + t

theorem set.Union₂_mul {α : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_6} [has_mul α] (s : Π (i : ι), κ i → set α) (t : set α) :

(⋃ (i : ι) (j : κ i), s i j) * t = ⋃ (i : ι) (j : κ i), s i j * t

theorem set.add_Union₂ {α : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_6} [has_add α] (s : set α) (t : Π (i : ι), κ i → set α) :

(s + ⋃ (i : ι) (j : κ i), t i j) = ⋃ (i : ι) (j : κ i), s + t i j

theorem set.mul_Union₂ {α : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_6} [has_mul α] (s : set α) (t : Π (i : ι), κ i → set α) :

(s * ⋃ (i : ι) (j : κ i), t i j) = ⋃ (i : ι) (j : κ i), s * t i j

theorem set.Inter_add_subset {α : Type u_2} {ι : Sort u_5} [has_add α] (s : ι → set α) (t : set α) :

(⋂ (i : ι), s i) + t ⊆ ⋂ (i : ι), s i + t

theorem set.Inter_mul_subset {α : Type u_2} {ι : Sort u_5} [has_mul α] (s : ι → set α) (t : set α) :

(⋂ (i : ι), s i) * t ⊆ ⋂ (i : ι), s i * t

theorem set.add_Inter_subset {α : Type u_2} {ι : Sort u_5} [has_add α] (s : set α) (t : ι → set α) :

(s + ⋂ (i : ι), t i) ⊆ ⋂ (i : ι), s + t i

theorem set.mul_Inter_subset {α : Type u_2} {ι : Sort u_5} [has_mul α] (s : set α) (t : ι → set α) :

(s * ⋂ (i : ι), t i) ⊆ ⋂ (i : ι), s * t i

theorem set.Inter₂_mul_subset {α : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_6} [has_mul α] (s : Π (i : ι), κ i → set α) (t : set α) :

(⋂ (i : ι) (j : κ i), s i j) * t ⊆ ⋂ (i : ι) (j : κ i), s i j * t

theorem set.Inter₂_add_subset {α : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_6} [has_add α] (s : Π (i : ι), κ i → set α) (t : set α) :

(⋂ (i : ι) (j : κ i), s i j) + t ⊆ ⋂ (i : ι) (j : κ i), s i j + t

theorem set.add_Inter₂_subset {α : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_6} [has_add α] (s : set α) (t : Π (i : ι), κ i → set α) :

(s + ⋂ (i : ι) (j : κ i), t i j) ⊆ ⋂ (i : ι) (j : κ i), s + t i j

theorem set.mul_Inter₂_subset {α : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_6} [has_mul α] (s : set α) (t : Π (i : ι), κ i → set α) :

(s * ⋂ (i : ι) (j : κ i), t i j) ⊆ ⋂ (i : ι) (j : κ i), s * t i j

theorem set.finite.mul {α : Type u_2} [has_mul α] {s t : set α} :

s.finite → t.finite → (s * t).finite

theorem set.finite.add {α : Type u_2} [has_add α] {s t : set α} :

s.finite → t.finite → (s + t).finite

def set.fintype_add {α : Type u_2} [has_add α] [decidable_eq α] (s t : set α) [fintype ↥s] [fintype ↥t] :

fintype ↥(s + 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 α) [fintype ↥s] [fintype ↥t] :

fintype ↥(s * t)

Multiplication preserves finiteness.

Equations

s.fintype_mul t = set.fintype_image2 (λ (a b : α), a * b) s t

def set.singleton_mul_hom {α : Type u_2} [has_mul α] :

α →ₙ* set α

The singleton operation as a mul_hom.

Equations

set.singleton_mul_hom = {to_fun := has_singleton.singleton set.has_singleton, map_mul' := _}

def set.singleton_add_hom {α : Type u_2} [has_add α] :

add_hom α (set α)

The singleton operation as an add_hom.

Equations

set.singleton_add_hom = {to_fun := has_singleton.singleton set.has_singleton, map_add' := _}

@[simp]

theorem set.coe_singleton_add_hom {α : Type u_2} [has_add α] :

⇑set.singleton_add_hom = has_singleton.singleton

@[simp]

theorem set.coe_singleton_mul_hom {α : Type u_2} [has_mul α] :

⇑set.singleton_mul_hom = has_singleton.singleton

@[simp]

theorem set.singleton_add_hom_apply {α : Type u_2} [has_add α] (a : α) :

⇑set.singleton_add_hom a = {a}

@[simp]

theorem set.singleton_mul_hom_apply {α : Type u_2} [has_mul α] (a : α) :

⇑set.singleton_mul_hom a = {a}

@[simp]

theorem set.image_op_add {α : Type u_2} [has_add α] {s t : set α} :

add_opposite.op '' (s + t) = add_opposite.op '' t + add_opposite.op '' s

@[simp]

theorem set.image_op_mul {α : Type u_2} [has_mul α] {s t : set α} :

mul_opposite.op '' (s * t) = mul_opposite.op '' t * mul_opposite.op '' s

Set subtraction/division #

@[protected]

def set.has_div {α : Type u_2} [has_div α] :

has_div (set α)

The pointwise division of sets s / t is defined as {x / y | x ∈ s, y ∈ t} in locale pointwise.

Equations

set.has_div = {div := set.image2 has_div.div}

@[protected]

def set.has_sub {α : Type u_2} [has_sub α] :

has_sub (set α)

The pointwise subtraction of sets s - t is defined as {x - y | x ∈ s, y ∈ t} in locale pointwise.

Equations

set.has_sub = {sub := set.image2 has_sub.sub}

@[simp]

theorem set.image2_sub {α : Type u_2} [has_sub α] {s t : set α} :

set.image2 has_sub.sub s t = s - t

@[simp]

theorem set.image2_div {α : Type u_2} [has_div α] {s t : set α} :

set.image2 has_div.div s t = s / t

theorem set.mem_sub {α : Type u_2} [has_sub α] {s t : set α} {a : α} :

a ∈ s - t ↔ ∃ (x y : α), x ∈ s ∧ y ∈ t ∧ x - y = a

theorem set.mem_div {α : Type u_2} [has_div α] {s t : set α} {a : α} :

a ∈ s / t ↔ ∃ (x y : α), x ∈ s ∧ y ∈ t ∧ x / y = a

theorem set.sub_mem_sub {α : Type u_2} [has_sub α] {s t : set α} {a b : α} :

a ∈ s → b ∈ t → a - b ∈ s - t

theorem set.div_mem_div {α : Type u_2} [has_div α] {s t : set α} {a b : α} :

a ∈ s → b ∈ t → a / b ∈ s / t

theorem set.image_div_prod {α : Type u_2} [has_div α] {s t : set α} :

(λ (x : α × α), x.fst / x.snd) '' s ×ˢ t = s / t

@[simp]

theorem set.empty_div {α : Type u_2} [has_div α] {s : set α} :

@[simp]

theorem set.empty_sub {α : Type u_2} [has_sub α] {s : set α} :

@[simp]

theorem set.sub_empty {α : Type u_2} [has_sub α] {s : set α} :

@[simp]

theorem set.div_empty {α : Type u_2} [has_div α] {s : set α} :

@[simp]

theorem set.div_eq_empty {α : Type u_2} [has_div α] {s t : set α} :

s / t = ∅ ↔ s = ∅ ∨ t = ∅

@[simp]

theorem set.sub_eq_empty {α : Type u_2} [has_sub α] {s t : set α} :

s - t = ∅ ↔ s = ∅ ∨ t = ∅

@[simp]

theorem set.div_nonempty {α : Type u_2} [has_div α] {s t : set α} :

(s / t).nonempty ↔ s.nonempty ∧ t.nonempty

@[simp]

theorem set.sub_nonempty {α : Type u_2} [has_sub α] {s t : set α} :

(s - t).nonempty ↔ s.nonempty ∧ t.nonempty

theorem set.nonempty.div {α : Type u_2} [has_div α] {s t : set α} :

s.nonempty → t.nonempty → (s / t).nonempty

theorem set.nonempty.sub {α : Type u_2} [has_sub α] {s t : set α} :

s.nonempty → t.nonempty → (s - t).nonempty

theorem set.nonempty.of_sub_left {α : Type u_2} [has_sub α] {s t : set α} :

(s - t).nonempty → s.nonempty

theorem set.nonempty.of_div_left {α : Type u_2} [has_div α] {s t : set α} :

(s / t).nonempty → s.nonempty

theorem set.nonempty.of_div_right {α : Type u_2} [has_div α] {s t : set α} :

(s / t).nonempty → t.nonempty

theorem set.nonempty.of_sub_right {α : Type u_2} [has_sub α] {s t : set α} :

(s - t).nonempty → t.nonempty

@[simp]

theorem set.div_singleton {α : Type u_2} [has_div α] {s : set α} {b : α} :

s / {b} = (λ (_x : α), _x / b) '' s

@[simp]

theorem set.sub_singleton {α : Type u_2} [has_sub α] {s : set α} {b : α} :

s - {b} = (λ (_x : α), _x - b) '' s

@[simp]

theorem set.singleton_div {α : Type u_2} [has_div α] {t : set α} {a : α} :

{a} / t = has_div.div a '' t

@[simp]

theorem set.singleton_sub {α : Type u_2} [has_sub α] {t : set α} {a : α} :

{a} - t = has_sub.sub a '' t

@[simp]

theorem set.singleton_sub_singleton {α : Type u_2} [has_sub α] {a b : α} :

{a} - {b} = {a - b}

@[simp]

theorem set.singleton_div_singleton {α : Type u_2} [has_div α] {a b : α} :

{a} / {b} = {a / b}

theorem set.div_subset_div {α : Type u_2} [has_div α] {s₁ s₂ t₁ t₂ : set α} :

s₁ ⊆ t₁ → s₂ ⊆ t₂ → s₁ / s₂ ⊆ t₁ / t₂

theorem set.sub_subset_sub {α : Type u_2} [has_sub α] {s₁ s₂ t₁ t₂ : set α} :

s₁ ⊆ t₁ → s₂ ⊆ t₂ → s₁ - s₂ ⊆ t₁ - t₂

theorem set.div_subset_div_left {α : Type u_2} [has_div α] {s t₁ t₂ : set α} :

t₁ ⊆ t₂ → s / t₁ ⊆ s / t₂

theorem set.sub_subset_sub_left {α : Type u_2} [has_sub α] {s t₁ t₂ : set α} :

t₁ ⊆ t₂ → s - t₁ ⊆ s - t₂

theorem set.sub_subset_sub_right {α : Type u_2} [has_sub α] {s₁ s₂ t : set α} :

s₁ ⊆ s₂ → s₁ - t ⊆ s₂ - t

theorem set.div_subset_div_right {α : Type u_2} [has_div α] {s₁ s₂ t : set α} :

s₁ ⊆ s₂ → s₁ / t ⊆ s₂ / t

theorem set.div_subset_iff {α : Type u_2} [has_div α] {s t u : set α} :

s / t ⊆ u ↔ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ t → x / y ∈ u

theorem set.sub_subset_iff {α : Type u_2} [has_sub α] {s t u : set α} :

s - t ⊆ u ↔ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ t → x - y ∈ u

theorem set.union_div {α : Type u_2} [has_div α] {s₁ s₂ t : set α} :

(s₁ ∪ s₂) / t = s₁ / t ∪ s₂ / t

theorem set.union_sub {α : Type u_2} [has_sub α] {s₁ s₂ t : set α} :

s₁ ∪ s₂ - t = s₁ - t ∪ (s₂ - t)

theorem set.div_union {α : Type u_2} [has_div α] {s t₁ t₂ : set α} :

s / (t₁ ∪ t₂) = s / t₁ ∪ s / t₂

theorem set.sub_union {α : Type u_2} [has_sub α] {s t₁ t₂ : set α} :

s - (t₁ ∪ t₂) = s - t₁ ∪ (s - t₂)

theorem set.inter_div_subset {α : Type u_2} [has_div α] {s₁ s₂ t : set α} :

s₁ ∩ s₂ / t ⊆ s₁ / t ∩ (s₂ / t)

theorem set.inter_sub_subset {α : Type u_2} [has_sub α] {s₁ s₂ t : set α} :

s₁ ∩ s₂ - t ⊆ (s₁ - t) ∩ (s₂ - t)

theorem set.div_inter_subset {α : Type u_2} [has_div α] {s t₁ t₂ : set α} :

s / (t₁ ∩ t₂) ⊆ s / t₁ ∩ (s / t₂)

theorem set.sub_inter_subset {α : Type u_2} [has_sub α] {s t₁ t₂ : set α} :

s - t₁ ∩ t₂ ⊆ (s - t₁) ∩ (s - t₂)

theorem set.Union_sub_left_image {α : Type u_2} [has_sub α] {s t : set α} :

(⋃ (a : α) (H : a ∈ s), has_sub.sub a '' t) = s - t

theorem set.Union_div_left_image {α : Type u_2} [has_div α] {s t : set α} :

(⋃ (a : α) (H : a ∈ s), has_div.div a '' t) = s / t

theorem set.Union_div_right_image {α : Type u_2} [has_div α] {s t : set α} :

(⋃ (a : α) (H : a ∈ t), (λ (_x : α), _x / a) '' s) = s / t

theorem set.Union_sub_right_image {α : Type u_2} [has_sub α] {s t : set α} :

(⋃ (a : α) (H : a ∈ t), (λ (_x : α), _x - a) '' s) = s - t

theorem set.Union_div {α : Type u_2} {ι : Sort u_5} [has_div α] (s : ι → set α) (t : set α) :

(⋃ (i : ι), s i) / t = ⋃ (i : ι), s i / t

theorem set.Union_sub {α : Type u_2} {ι : Sort u_5} [has_sub α] (s : ι → set α) (t : set α) :

(⋃ (i : ι), s i) - t = ⋃ (i : ι), s i - t

theorem set.sub_Union {α : Type u_2} {ι : Sort u_5} [has_sub α] (s : set α) (t : ι → set α) :

(s - ⋃ (i : ι), t i) = ⋃ (i : ι), s - t i

theorem set.div_Union {α : Type u_2} {ι : Sort u_5} [has_div α] (s : set α) (t : ι → set α) :

(s / ⋃ (i : ι), t i) = ⋃ (i : ι), s / t i

theorem set.Union₂_sub {α : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_6} [has_sub α] (s : Π (i : ι), κ i → set α) (t : set α) :

(⋃ (i : ι) (j : κ i), s i j) - t = ⋃ (i : ι) (j : κ i), s i j - t

theorem set.Union₂_div {α : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_6} [has_div α] (s : Π (i : ι), κ i → set α) (t : set α) :

(⋃ (i : ι) (j : κ i), s i j) / t = ⋃ (i : ι) (j : κ i), s i j / t

theorem set.div_Union₂ {α : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_6} [has_div α] (s : set α) (t : Π (i : ι), κ i → set α) :

(s / ⋃ (i : ι) (j : κ i), t i j) = ⋃ (i : ι) (j : κ i), s / t i j

theorem set.sub_Union₂ {α : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_6} [has_sub α] (s : set α) (t : Π (i : ι), κ i → set α) :

(s - ⋃ (i : ι) (j : κ i), t i j) = ⋃ (i : ι) (j : κ i), s - t i j

theorem set.Inter_sub_subset {α : Type u_2} {ι : Sort u_5} [has_sub α] (s : ι → set α) (t : set α) :

(⋂ (i : ι), s i) - t ⊆ ⋂ (i : ι), s i - t

theorem set.Inter_div_subset {α : Type u_2} {ι : Sort u_5} [has_div α] (s : ι → set α) (t : set α) :

(⋂ (i : ι), s i) / t ⊆ ⋂ (i : ι), s i / t

theorem set.sub_Inter_subset {α : Type u_2} {ι : Sort u_5} [has_sub α] (s : set α) (t : ι → set α) :

(s - ⋂ (i : ι), t i) ⊆ ⋂ (i : ι), s - t i

theorem set.div_Inter_subset {α : Type u_2} {ι : Sort u_5} [has_div α] (s : set α) (t : ι → set α) :

(s / ⋂ (i : ι), t i) ⊆ ⋂ (i : ι), s / t i

theorem set.Inter₂_div_subset {α : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_6} [has_div α] (s : Π (i : ι), κ i → set α) (t : set α) :

(⋂ (i : ι) (j : κ i), s i j) / t ⊆ ⋂ (i : ι) (j : κ i), s i j / t

theorem set.Inter₂_sub_subset {α : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_6} [has_sub α] (s : Π (i : ι), κ i → set α) (t : set α) :

(⋂ (i : ι) (j : κ i), s i j) - t ⊆ ⋂ (i : ι) (j : κ i), s i j - t

theorem set.div_Inter₂_subset {α : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_6} [has_div α] (s : set α) (t : Π (i : ι), κ i → set α) :

(s / ⋂ (i : ι) (j : κ i), t i j) ⊆ ⋂ (i : ι) (j : κ i), s / t i j

theorem set.sub_Inter₂_subset {α : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_6} [has_sub α] (s : set α) (t : Π (i : ι), κ i → set α) :

(s - ⋂ (i : ι) (j : κ i), t i j) ⊆ ⋂ (i : ι) (j : κ i), s - t i j

@[protected]

def set.has_nsmul {α : Type u_2} [has_zero α] [has_add α] :

has_smul ℕ (set α)

Repeated pointwise addition (not the same as pointwise repeated addition!) of a finset. See note [pointwise nat action].

Equations

set.has_nsmul = {smul := nsmul_rec set.has_add}

@[protected]

def set.has_npow {α : Type u_2} [has_one α] [has_mul α] :

has_pow (set α) ℕ

Repeated pointwise multiplication (not the same as pointwise repeated multiplication!) of a set. See note [pointwise nat action].

Equations

set.has_npow = {pow := λ (s : set α) (n : ℕ), npow_rec n s}

@[protected]

def set.has_zsmul {α : Type u_2} [has_zero α] [has_add α] [has_neg α] :

has_smul ℤ (set α)

Repeated pointwise addition/subtraction (not the same as pointwise repeated addition/subtraction!) of a set. See note [pointwise nat action].

Equations

set.has_zsmul = {smul := zsmul_rec set.has_neg}

@[protected]

def set.has_zpow {α : Type u_2} [has_one α] [has_mul α] [has_inv α] :

has_pow (set α) ℤ

Repeated pointwise multiplication/division (not the same as pointwise repeated multiplication/division!) of a set. See note [pointwise nat action].

Equations

set.has_zpow = {pow := λ (s : set α) (n : ℤ), zpow_rec n s}

@[protected]

def set.add_semigroup {α : Type u_2} [add_semigroup α] :

add_semigroup (set α)

set α is an add_semigroup under pointwise operations if α is.

Equations

set.add_semigroup = {add := has_add.add set.has_add, add_assoc := _}

@[protected]

def set.semigroup {α : Type u_2} [semigroup α] :

semigroup (set α)

set α is a semigroup under pointwise operations if α is.

Equations

set.semigroup = {mul := has_mul.mul set.has_mul, mul_assoc := _}

@[protected]

def set.add_comm_semigroup {α : Type u_2} [add_comm_semigroup α] :

add_comm_semigroup (set α)

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]

def set.comm_semigroup {α : Type u_2} [comm_semigroup α] :

comm_semigroup (set α)

set α is a comm_semigroup under pointwise operations if α is.

Equations

set.comm_semigroup = {mul := semigroup.mul set.semigroup, mul_assoc := _, mul_comm := _}

@[protected]

def set.add_zero_class {α : Type u_2} [add_zero_class α] :

add_zero_class (set α)

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]

def set.mul_one_class {α : Type u_2} [mul_one_class α] :

mul_one_class (set α)

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 := _}

theorem set.subset_mul_left {α : Type u_2} [mul_one_class α] (s : set α) {t : set α} (ht : 1 ∈ t) :

s ⊆ s * t

theorem set.subset_add_left {α : Type u_2} [add_zero_class α] (s : set α) {t : set α} (ht : 0 ∈ t) :

s ⊆ s + t

theorem set.subset_add_right {α : Type u_2} [add_zero_class α] {s : set α} (t : set α) (hs : 0 ∈ s) :

t ⊆ s + t

theorem set.subset_mul_right {α : Type u_2} [mul_one_class α] {s : set α} (t : set α) (hs : 1 ∈ s) :

t ⊆ s * t

def set.singleton_monoid_hom {α : Type u_2} [mul_one_class α] :

α →* set α

The singleton operation as a monoid_hom.

Equations

set.singleton_monoid_hom = {to_fun := set.singleton_mul_hom.to_fun, map_one' := _, map_mul' := _}

def set.singleton_add_monoid_hom {α : Type u_2} [add_zero_class α] :

α →+ set α

The singleton operation as an add_monoid_hom.

Equations

set.singleton_add_monoid_hom = {to_fun := set.singleton_add_hom.to_fun, map_zero' := _, map_add' := _}

@[simp]

theorem set.coe_singleton_monoid_hom {α : Type u_2} [mul_one_class α] :

⇑set.singleton_monoid_hom = has_singleton.singleton

@[simp]

theorem set.coe_singleton_add_monoid_hom {α : Type u_2} [add_zero_class α] :

⇑set.singleton_add_monoid_hom = has_singleton.singleton

@[simp]

theorem set.singleton_add_monoid_hom_apply {α : Type u_2} [add_zero_class α] (a : α) :

⇑set.singleton_add_monoid_hom a = {a}

@[simp]

theorem set.singleton_monoid_hom_apply {α : Type u_2} [mul_one_class α] (a : α) :

⇑set.singleton_monoid_hom a = {a}

@[protected]

def set.monoid {α : Type u_2} [monoid α] :

monoid (set α)

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]

def set.add_monoid {α : Type u_2} [add_monoid α] :

add_monoid (set α)

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]

def set.decidable_mem_add {α : Type u_2} [add_monoid α] {s t : set α} [fintype α] [decidable_eq α] [decidable_pred (λ (_x : α), _x ∈ s)] [decidable_pred (λ (_x : α), _x ∈ t)] :

decidable_pred (λ (_x : α), _x ∈ s + t)

Equations

set.decidable_mem_add = λ (_x : α), decidable_of_iff (∃ (x y : α), x ∈ s ∧ y ∈ t ∧ x + y = _x) _

@[protected, instance]

def set.decidable_mem_mul {α : Type u_2} [monoid α] {s t : set α} [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_nsmul {α : Type u_2} [add_monoid α] {s : set α} [fintype α] [decidable_eq α] [decidable_pred (λ (_x : α), _x ∈ s)] (n : ℕ) :

decidable_pred (λ (_x : α), _x ∈ n • s)

Equations

set.decidable_mem_nsmul n = nat.rec (set.decidable_mem_nsmul._proof_1.mpr (set.decidable_mem_nsmul._proof_2.mpr (λ (a : α), _inst_3 a 0))) (λ (n : ℕ) (ih : decidable_pred (λ (_x : α), _x ∈ n • s)), let _inst : decidable_pred (λ (_x : α), _x ∈ n • s) := ih in _.mpr (λ (a : α), set.decidable_mem_add a)) n

@[protected, instance]

def set.decidable_mem_pow {α : Type u_2} [monoid α] {s : set α} [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.nsmul_mem_nsmul {α : Type u_2} [add_monoid α] {s : set α} {a : α} (ha : a ∈ s) (n : ℕ) :

n • a ∈ n • s

theorem set.pow_mem_pow {α : Type u_2} [monoid α] {s : set α} {a : α} (ha : a ∈ s) (n : ℕ) :

a ^ n ∈ s ^ n

theorem set.nsmul_subset_nsmul {α : Type u_2} [add_monoid α] {s t : set α} (hst : s ⊆ t) (n : ℕ) :

n • s ⊆ n • t

theorem set.pow_subset_pow {α : Type u_2} [monoid α] {s t : set α} (hst : s ⊆ t) (n : ℕ) :

s ^ n ⊆ t ^ n

theorem set.pow_subset_pow_of_one_mem {α : Type u_2} [monoid α] {s : set α} {m n : ℕ} (hs : 1 ∈ s) :

m ≤ n → s ^ m ⊆ s ^ n

theorem set.nsmul_subset_nsmul_of_zero_mem {α : Type u_2} [add_monoid α] {s : set α} {m n : ℕ} (hs : 0 ∈ s) :

m ≤ n → m • s ⊆ n • s

theorem set.mem_prod_list_of_fn {α : Type u_2} [monoid α] {n : ℕ} {a : α} {s : fin n → set α} :

a ∈ (list.of_fn s).prod ↔ ∃ (f : Π (i : fin n), ↥(s i)), (list.of_fn (λ (i : fin n), ↑(f i))).prod = a

theorem set.mem_sum_list_of_fn {α : Type u_2} [add_monoid α] {n : ℕ} {a : α} {s : fin n → set α} :

a ∈ (list.of_fn s).sum ↔ ∃ (f : Π (i : fin n), ↥(s i)), (list.of_fn (λ (i : fin n), ↑(f i))).sum = a

theorem set.mem_list_sum {α : Type u_2} [add_monoid α] {l : list (set α)} {a : α} :

a ∈ l.sum ↔ ∃ (l' : list (Σ (s : set α), ↥s)), (list.map (λ (x : Σ (s : set α), ↥s), ↑(x.snd)) l').sum = a ∧ list.map sigma.fst l' = l

theorem set.mem_list_prod {α : Type u_2} [monoid α] {l : list (set α)} {a : α} :

a ∈ l.prod ↔ ∃ (l' : list (Σ (s : set α), ↥s)), (list.map (λ (x : Σ (s : set α), ↥s), ↑(x.snd)) l').prod = a ∧ list.map sigma.fst l' = l

theorem set.mem_nsmul {α : Type u_2} [add_monoid α] {s : set α} {a : α} {n : ℕ} :

a ∈ n • s ↔ ∃ (f : fin n → ↥s), (list.of_fn (λ (i : fin n), ↑(f i))).sum = a

theorem set.mem_pow {α : Type u_2} [monoid α] {s : set α} {a : α} {n : ℕ} :

a ∈ s ^ n ↔ ∃ (f : fin n → ↥s), (list.of_fn (λ (i : fin n), ↑(f i))).prod = a

@[simp]

theorem set.empty_pow {α : Type u_2} [monoid α] {n : ℕ} (hn : n ≠ 0) :

@[simp]

theorem set.empty_nsmul {α : Type u_2} [add_monoid α] {n : ℕ} (hn : n ≠ 0) :

n • ∅ = ∅

theorem set.mul_univ_of_one_mem {α : Type u_2} [monoid α] {s : set α} (hs : 1 ∈ s) :

s * set.univ = set.univ

theorem set.add_univ_of_zero_mem {α : Type u_2} [add_monoid α] {s : set α} (hs : 0 ∈ s) :

s + set.univ = set.univ

theorem set.univ_add_of_zero_mem {α : Type u_2} [add_monoid α] {t : set α} (ht : 0 ∈ t) :

set.univ + t = set.univ

theorem set.univ_mul_of_one_mem {α : Type u_2} [monoid α] {t : set α} (ht : 1 ∈ t) :

set.univ * t = set.univ

@[simp]

theorem set.univ_add_univ {α : Type u_2} [add_monoid α] :

set.univ + set.univ = set.univ

@[simp]

theorem set.univ_mul_univ {α : Type u_2} [monoid α] :

set.univ * set.univ = set.univ

@[simp]

theorem set.nsmul_univ {α : Type u_1} [add_monoid α] {n : ℕ} :

n ≠ 0 → n • set.univ = set.univ

@[simp]

theorem set.univ_pow {α : Type u_2} [monoid α] {n : ℕ} :

n ≠ 0 → set.univ ^ n = set.univ

@[protected]

theorem is_unit.set {α : Type u_2} [monoid α] {a : α} :

is_unit a → is_unit {a}

@[protected]

theorem is_add_unit.set {α : Type u_2} [add_monoid α] {a : α} :

is_add_unit a → is_add_unit {a}

@[protected]

def set.comm_monoid {α : Type u_2} [comm_monoid α] :

comm_monoid (set α)

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]

def set.add_comm_monoid {α : Type u_2} [add_comm_monoid α] :

add_comm_monoid (set α)

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 := _}

@[protected]

theorem set.mul_eq_one_iff {α : Type u_2} [division_monoid α] {s t : set α} :

s * t = 1 ↔ ∃ (a b : α), s = {a} ∧ t = {b} ∧ a * b = 1

@[protected]

theorem set.add_eq_zero_iff {α : Type u_2} [subtraction_monoid α] {s t : set α} :

s + t = 0 ↔ ∃ (a b : α), s = {a} ∧ t = {b} ∧ a + b = 0

@[protected]

def set.subtraction_monoid {α : Type u_2} [subtraction_monoid α] :

subtraction_monoid (set α)

set α is a subtraction monoid under pointwise operations if α is.

Equations

set.subtraction_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_involutive_neg.neg set.has_involutive_neg, sub := has_sub.sub set.has_sub, sub_eq_add_neg := _, zsmul := sub_neg_monoid.zsmul._default add_monoid.add set.subtraction_monoid._proof_7 add_monoid.zero set.subtraction_monoid._proof_8 set.subtraction_monoid._proof_9 add_monoid.nsmul set.subtraction_monoid._proof_10 set.subtraction_monoid._proof_11 has_involutive_neg.neg, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, neg_neg := _, neg_add_rev := _, neg_eq_of_add := _}

@[protected]

def set.division_monoid {α : Type u_2} [division_monoid α] :

division_monoid (set α)

set α is a division monoid under pointwise operations if α is.

Equations

set.division_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_involutive_inv.inv set.has_involutive_inv, div := has_div.div set.has_div, div_eq_mul_inv := _, zpow := div_inv_monoid.zpow._default monoid.mul set.division_monoid._proof_7 monoid.one set.division_monoid._proof_8 set.division_monoid._proof_9 monoid.npow set.division_monoid._proof_10 set.division_monoid._proof_11 has_involutive_inv.inv, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, inv_inv := _, mul_inv_rev := _, inv_eq_of_mul := _}

@[simp]

theorem set.is_unit_iff {α : Type u_2} [division_monoid α] {s : set α} :

is_unit s ↔ ∃ (a : α), s = {a} ∧ is_unit a

@[simp]

theorem set.is_add_unit_iff {α : Type u_2} [subtraction_monoid α] {s : set α} :

is_add_unit s ↔ ∃ (a : α), s = {a} ∧ is_add_unit a

@[protected]

def set.division_comm_monoid {α : Type u_2} [division_comm_monoid α] :

division_comm_monoid (set α)

set α is a commutative division monoid under pointwise operations if α is.

Equations

set.division_comm_monoid = {mul := division_monoid.mul set.division_monoid, mul_assoc := _, one := division_monoid.one set.division_monoid, one_mul := _, mul_one := _, npow := division_monoid.npow set.division_monoid, npow_zero' := _, npow_succ' := _, inv := division_monoid.inv set.division_monoid, div := division_monoid.div set.division_monoid, div_eq_mul_inv := _, zpow := division_monoid.zpow set.division_monoid, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, inv_inv := _, mul_inv_rev := _, inv_eq_of_mul := _, mul_comm := _}

@[protected]

def set.subtraction_comm_monoid {α : Type u_2} [subtraction_comm_monoid α] :

subtraction_comm_monoid (set α)

set α is a commutative subtraction monoid under pointwise operations if α is.

Equations

set.subtraction_comm_monoid = {add := subtraction_monoid.add set.subtraction_monoid, add_assoc := _, zero := subtraction_monoid.zero set.subtraction_monoid, zero_add := _, add_zero := _, nsmul := subtraction_monoid.nsmul set.subtraction_monoid, nsmul_zero' := _, nsmul_succ' := _, neg := subtraction_monoid.neg set.subtraction_monoid, sub := subtraction_monoid.sub set.subtraction_monoid, sub_eq_add_neg := _, zsmul := subtraction_monoid.zsmul set.subtraction_monoid, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, neg_neg := _, neg_add_rev := _, neg_eq_of_add := _, add_comm := _}

@[protected]

def set.has_distrib_neg {α : Type u_2} [has_mul α] [has_distrib_neg α] :

has_distrib_neg (set α)

set α has distributive negation if α has.

Equations

set.has_distrib_neg = {neg := has_involutive_neg.neg set.has_involutive_neg, neg_neg := _, neg_mul := _, mul_neg := _}

Note that set α is not a distrib because s * t + s * u has cross terms that s * (t + u) lacks.

theorem set.mul_add_subset {α : Type u_2} [distrib α] (s t u : set α) :

s * (t + u) ⊆ s * t + s * u

theorem set.add_mul_subset {α : Type u_2} [distrib α] (s t u : set α) :

(s + t) * u ⊆ s * u + t * u

Note that set is not a mul_zero_class because 0 * ∅ ≠ 0.

theorem set.mul_zero_subset {α : Type u_2} [mul_zero_class α] (s : set α) :

s * 0 ⊆ 0

theorem set.zero_mul_subset {α : Type u_2} [mul_zero_class α] (s : set α) :

0 * s ⊆ 0

theorem set.nonempty.mul_zero {α : Type u_2} [mul_zero_class α] {s : set α} (hs : s.nonempty) :

s * 0 = 0

theorem set.nonempty.zero_mul {α : Type u_2} [mul_zero_class α] {s : set α} (hs : s.nonempty) :

0 * s = 0

Note that set is not a group because s / s ≠ 1 in general.

@[simp]

theorem set.one_mem_div_iff {α : Type u_2} [group α] {s t : set α} :

1 ∈ s / t ↔ ¬disjoint s t

@[simp]

theorem set.zero_mem_sub_iff {α : Type u_2} [add_group α] {s t : set α} :

0 ∈ s - t ↔ ¬disjoint s t

theorem set.not_zero_mem_sub_iff {α : Type u_2} [add_group α] {s t : set α} :

0 ∉ s - t ↔ disjoint s t

theorem set.not_one_mem_div_iff {α : Type u_2} [group α] {s t : set α} :

1 ∉ s / t ↔ disjoint s t

theorem disjoint.one_not_mem_div_set {α : Type u_2} [group α] {s t : set α} :

disjoint s t → 1 ∉ s / t

Alias of the reverse direction of set.not_one_mem_div_iff.

theorem disjoint.zero_not_mem_sub_set {α : Type u_2} [add_group α] {s t : set α} :

disjoint s t → 0 ∉ s - t

Alias of the reverse direction of set.not_one_mem_div_iff.

theorem set.nonempty.one_mem_div {α : Type u_2} [group α] {s : set α} (h : s.nonempty) :

1 ∈ s / s

theorem set.nonempty.zero_mem_sub {α : Type u_2} [add_group α] {s : set α} (h : s.nonempty) :

0 ∈ s - s

theorem set.is_unit_singleton {α : Type u_2} [group α] (a : α) :

theorem set.is_add_unit_singleton {α : Type u_2} [add_group α] (a : α) :

is_add_unit {a}

@[simp]

theorem set.is_add_unit_iff_singleton {α : Type u_2} [add_group α] {s : set α} :

is_add_unit s ↔ ∃ (a : α), s = {a}

@[simp]

theorem set.is_unit_iff_singleton {α : Type u_2} [group α] {s : set α} :

is_unit s ↔ ∃ (a : α), s = {a}

@[simp]

theorem set.image_add_left {α : Type u_2} [add_group α] {t : set α} {a : α} :

has_add.add a '' t = has_add.add (-a) ⁻¹' t

@[simp]

theorem set.image_mul_left {α : Type u_2} [group α] {t : set α} {a : α} :

has_mul.mul a '' t = has_mul.mul a⁻¹ ⁻¹' t

@[simp]

theorem set.image_mul_right {α : Type u_2} [group α] {t : set α} {b : α} :

(λ (_x : α), _x * b) '' t = (λ (_x : α), _x * b⁻¹) ⁻¹' t

@[simp]

theorem set.image_add_right {α : Type u_2} [add_group α] {t : set α} {b : α} :

(λ (_x : α), _x + b) '' t = (λ (_x : α), _x + -b) ⁻¹' t

theorem set.image_mul_left' {α : Type u_2} [group α] {t : set α} {a : α} :

(λ (b : α), a⁻¹ * b) '' t = (λ (b : α), a * b) ⁻¹' t

theorem set.image_add_left' {α : Type u_2} [add_group α] {t : set α} {a : α} :

(λ (b : α), -a + b) '' t = (λ (b : α), a + b) ⁻¹' t

theorem set.image_mul_right' {α : Type u_2} [group α] {t : set α} {b : α} :

(λ (_x : α), _x * b⁻¹) '' t = (λ (_x : α), _x * b) ⁻¹' t

theorem set.image_add_right' {α : Type u_2} [add_group α] {t : set α} {b : α} :

(λ (_x : α), _x + -b) '' t = (λ (_x : α), _x + b) ⁻¹' t

@[simp]

theorem set.preimage_mul_left_singleton {α : Type u_2} [group α] {a b : α} :

has_mul.mul a ⁻¹' {b} = {a⁻¹ * b}

@[simp]

theorem set.preimage_add_left_singleton {α : Type u_2} [add_group α] {a b : α} :

has_add.add a ⁻¹' {b} = {-a + b}

@[simp]

theorem set.preimage_mul_right_singleton {α : Type u_2} [group α] {a b : α} :

(λ (_x : α), _x * a) ⁻¹' {b} = {b * a⁻¹}

@[simp]

theorem set.preimage_add_right_singleton {α : Type u_2} [add_group α] {a b : α} :

(λ (_x : α), _x + a) ⁻¹' {b} = {b + -a}

@[simp]

theorem set.preimage_mul_left_one {α : Type u_2} [group α] {a : α} :

has_mul.mul a ⁻¹' 1 = {a⁻¹}

@[simp]

theorem set.preimage_add_left_zero {α : Type u_2} [add_group α] {a : α} :

has_add.add a ⁻¹' 0 = {-a}

@[simp]

theorem set.preimage_add_right_zero {α : Type u_2} [add_group α] {b : α} :

(λ (_x : α), _x + b) ⁻¹' 0 = {-b}

@[simp]

theorem set.preimage_mul_right_one {α : Type u_2} [group α] {b : α} :

(λ (_x : α), _x * b) ⁻¹' 1 = {b⁻¹}

theorem set.preimage_add_left_zero' {α : Type u_2} [add_group α] {a : α} :

(λ (b : α), -a + b) ⁻¹' 0 = {a}

theorem set.preimage_mul_left_one' {α : Type u_2} [group α] {a : α} :

(λ (b : α), a⁻¹ * b) ⁻¹' 1 = {a}

theorem set.preimage_add_right_zero' {α : Type u_2} [add_group α] {b : α} :

(λ (_x : α), _x + -b) ⁻¹' 0 = {b}

theorem set.preimage_mul_right_one' {α : Type u_2} [group α] {b : α} :

(λ (_x : α), _x * b⁻¹) ⁻¹' 1 = {b}

@[simp]

theorem set.mul_univ {α : Type u_2} [group α] {s : set α} (hs : s.nonempty) :

s * set.univ = set.univ

@[simp]

theorem set.add_univ {α : Type u_2} [add_group α] {s : set α} (hs : s.nonempty) :

s + set.univ = set.univ

@[simp]

theorem set.univ_mul {α : Type u_2} [group α] {t : set α} (ht : t.nonempty) :

set.univ * t = set.univ

@[simp]

theorem set.univ_add {α : Type u_2} [add_group α] {t : set α} (ht : t.nonempty) :

set.univ + t = set.univ

theorem set.div_zero_subset {α : Type u_2} [group_with_zero α] (s : set α) :

s / 0 ⊆ 0

theorem set.zero_div_subset {α : Type u_2} [group_with_zero α] (s : set α) :

0 / s ⊆ 0

theorem set.nonempty.div_zero {α : Type u_2} [group_with_zero α] {s : set α} (hs : s.nonempty) :

s / 0 = 0

theorem set.nonempty.zero_div {α : Type u_2} [group_with_zero α] {s : set α} (hs : s.nonempty) :

0 / s = 0

theorem set.image_add {F : Type u_1} {α : Type u_2} {β : Type u_3} [has_add α] [has_add β] [add_hom_class F α β] (m : F) {s t : set α} :

⇑m '' (s + t) = ⇑m '' s + ⇑m '' t

theorem set.image_mul {F : Type u_1} {α : Type u_2} {β : Type u_3} [has_mul α] [has_mul β] [mul_hom_class F α β] (m : F) {s t : set α} :

⇑m '' (s * t) = ⇑m '' s * ⇑m '' t

theorem set.preimage_mul_preimage_subset {F : Type u_1} {α : Type u_2} {β : Type u_3} [has_mul α] [has_mul β] [mul_hom_class F α β] (m : F) {s t : set β} :

⇑m ⁻¹' s * ⇑m ⁻¹' t ⊆ ⇑m ⁻¹' (s * t)

theorem set.preimage_add_preimage_subset {F : Type u_1} {α : Type u_2} {β : Type u_3} [has_add α] [has_add β] [add_hom_class F α β] (m : F) {s t : set β} :

⇑m ⁻¹' s + ⇑m ⁻¹' t ⊆ ⇑m ⁻¹' (s + t)

theorem set.image_div {F : Type u_1} {α : Type u_2} {β : Type u_3} [group α] [division_monoid β] [monoid_hom_class F α β] (m : F) {s t : set α} :

⇑m '' (s / t) = ⇑m '' s / ⇑m '' t

theorem set.image_sub {F : Type u_1} {α : Type u_2} {β : Type u_3} [add_group α] [subtraction_monoid β] [add_monoid_hom_class F α β] (m : F) {s t : set α} :

⇑m '' (s - t) = ⇑m '' s - ⇑m '' t

theorem set.preimage_div_preimage_subset {F : Type u_1} {α : Type u_2} {β : Type u_3} [group α] [division_monoid β] [monoid_hom_class F α β] (m : F) {s t : set β} :

⇑m ⁻¹' s / ⇑m ⁻¹' t ⊆ ⇑m ⁻¹' (s / t)

theorem set.preimage_sub_preimage_subset {F : Type u_1} {α : Type u_2} {β : Type u_3} [add_group α] [subtraction_monoid β] [add_monoid_hom_class F α β] (m : F) {s t : set β} :

⇑m ⁻¹' s - ⇑m ⁻¹' t ⊆ ⇑m ⁻¹' (s - t)

theorem set.bdd_above_add {α : Type u_2} [ordered_add_comm_monoid α] {A B : set α} :

bdd_above A → bdd_above B → bdd_above (A + B)

theorem set.bdd_above_mul {α : Type u_2} [ordered_comm_monoid α] {A B : set α} :

bdd_above A → bdd_above B → bdd_above (A * B)

theorem set.mem_finset_sum {α : Type u_2} {ι : Type u_5} [add_comm_monoid α] (t : finset ι) (f : ι → set α) (a : α) :

a ∈ t.sum (λ (i : ι), f i) ↔ ∃ (g : ι → α) (hg : ∀ {i : ι}, i ∈ t → g i ∈ f i), t.sum (λ (i : ι), g i) = 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 : α) :

a ∈ t.prod (λ (i : ι), f i) ↔ ∃ (g : ι → α) (hg : ∀ {i : ι}, i ∈ t → g i ∈ f i), t.prod (λ (i : ι), g i) = 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 ∈ finset.univ.prod (λ (i : ι), f i) ↔ ∃ (g : ι → α) (hg : ∀ (i : ι), g i ∈ f i), finset.univ.prod (λ (i : ι), g i) = 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 ∈ finset.univ.sum (λ (i : ι), f i) ↔ ∃ (g : ι → α) (hg : ∀ (i : ι), g i ∈ f i), finset.univ.sum (λ (i : ι), g i) = a

A version of set.mem_finset_sum with a simpler RHS for sums over a fintype.

theorem set.list_sum_mem_list_sum {α : Type u_2} {ι : Type u_5} [add_comm_monoid α] (t : list ι) (f : ι → set α) (g : ι → α) (hg : ∀ (i : ι), i ∈ t → g i ∈ f i) :

(list.map g t).sum ∈ (list.map f t).sum

An n-ary version of set.add_mem_add.

theorem set.list_prod_mem_list_prod {α : Type u_2} {ι : Type u_5} [comm_monoid α] (t : list ι) (f : ι → set α) (g : ι → α) (hg : ∀ (i : ι), i ∈ t → g i ∈ f i) :

(list.map g t).prod ∈ (list.map f t).prod

An n-ary version of set.mul_mem_mul.

theorem set.list_sum_subset_list_sum {α : Type u_2} {ι : Type u_5} [add_comm_monoid α] (t : list ι) (f₁ f₂ : ι → set α) (hf : ∀ (i : ι), i ∈ t → f₁ i ⊆ f₂ i) :

(list.map f₁ t).sum ⊆ (list.map f₂ t).sum

An n-ary version of set.add_subset_add.

theorem set.list_prod_subset_list_prod {α : Type u_2} {ι : Type u_5} [comm_monoid α] (t : list ι) (f₁ f₂ : ι → set α) (hf : ∀ (i : ι), i ∈ t → f₁ i ⊆ f₂ i) :

(list.map f₁ t).prod ⊆ (list.map f₂ t).prod

An n-ary version of set.mul_subset_mul.

theorem set.list_sum_singleton {M : Type u_1} [add_comm_monoid M] (s : list M) :

(list.map (λ (i : M), {i}) s).sum = {s.sum}

theorem set.list_prod_singleton {M : Type u_1} [comm_monoid M] (s : list M) :

(list.map (λ (i : M), {i}) s).prod = {s.prod}

theorem set.multiset_sum_mem_multiset_sum {α : Type u_2} {ι : Type u_5} [add_comm_monoid α] (t : multiset ι) (f : ι → set α) (g : ι → α) (hg : ∀ (i : ι), i ∈ t → g i ∈ f i) :

(multiset.map g t).sum ∈ (multiset.map f t).sum

An n-ary version of set.add_mem_add.

theorem set.multiset_prod_mem_multiset_prod {α : Type u_2} {ι : Type u_5} [comm_monoid α] (t : multiset ι) (f : ι → set α) (g : ι → α) (hg : ∀ (i : ι), i ∈ t → g i ∈ f i) :

(multiset.map g t).prod ∈ (multiset.map f t).prod

An n-ary version of set.mul_mem_mul.

theorem set.multiset_prod_subset_multiset_prod {α : Type u_2} {ι : Type u_5} [comm_monoid α] (t : multiset ι) (f₁ f₂ : ι → set α) (hf : ∀ (i : ι), i ∈ t → f₁ i ⊆ f₂ i) :

(multiset.map f₁ t).prod ⊆ (multiset.map f₂ t).prod

An n-ary version of set.mul_subset_mul.

theorem set.multiset_sum_subset_multiset_sum {α : Type u_2} {ι : Type u_5} [add_comm_monoid α] (t : multiset ι) (f₁ f₂ : ι → set α) (hf : ∀ (i : ι), i ∈ t → f₁ i ⊆ f₂ i) :

(multiset.map f₁ t).sum ⊆ (multiset.map f₂ t).sum

An n-ary version of set.add_subset_add.

theorem set.multiset_sum_singleton {M : Type u_1} [add_comm_monoid M] (s : multiset M) :

(multiset.map (λ (i : M), {i}) s).sum = {s.sum}

theorem set.multiset_prod_singleton {M : Type u_1} [comm_monoid M] (s : multiset M) :

(multiset.map (λ (i : M), {i}) s).prod = {s.prod}

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) :

t.prod (λ (i : ι), g i) ∈ t.prod (λ (i : ι), f i)

An 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) :

t.sum (λ (i : ι), g i) ∈ t.sum (λ (i : ι), f i)

An 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) :

t.prod (λ (i : ι), f₁ i) ⊆ t.prod (λ (i : ι), f₂ i)

An 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) :

t.sum (λ (i : ι), f₁ i) ⊆ t.sum (λ (i : ι), f₂ i)

An 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) :

s.prod (λ (i : ι), {I i}) = {s.prod (λ (i : ι), I i)}

theorem set.finset_sum_singleton {M : Type u_1} {ι : Type u_2} [add_comm_monoid M] (s : finset ι) (I : ι → M) :

s.sum (λ (i : ι), {I i}) = {s.sum (λ (i : ι), I i)}

TODO: define decidable_mem_finset_prod and decidable_mem_finset_sum.

Translation/scaling of sets #

@[protected]

def set.has_smul_set {α : Type u_2} {β : Type u_3} [has_smul α β] :

has_smul α (set β)

The dilation of set x • s is defined as {x • y | y ∈ s} in locale pointwise.

Equations

set.has_smul_set = {smul := λ (a : α), set.image (has_smul.smul a)}

@[protected]

def set.has_vadd_set {α : Type u_2} {β : Type u_3} [has_vadd α β] :

has_vadd α (set β)

The translation of set x +ᵥ s is defined as {x +ᵥ y | y ∈ s} in locale pointwise.

Equations

set.has_vadd_set = {vadd := λ (a : α), set.image (has_vadd.vadd a)}

@[protected]

def set.has_smul {α : Type u_2} {β : Type u_3} [has_smul α β] :

has_smul (set α) (set β)

The pointwise scalar multiplication of sets s • t is defined as {x • y | x ∈ s, y ∈ t} in locale pointwise.

Equations

set.has_smul = {smul := set.image2 has_smul.smul}

@[protected]

def set.has_vadd {α : Type u_2} {β : Type u_3} [has_vadd α β] :

has_vadd (set α) (set β)

The pointwise scalar addition of sets s +ᵥ t is defined as {x +ᵥ y | x ∈ s, y ∈ t} in locale pointwise.

Equations

set.has_vadd = {vadd := set.image2 has_vadd.vadd}

@[simp]

theorem set.image2_smul {α : Type u_2} {β : Type u_3} [has_smul α β] {s : set α} {t : set β} :

set.image2 has_smul.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.image_smul_prod {α : Type u_2} {β : Type u_3} [has_smul α β] {s : set α} {t : set β} :

(λ (x : α × β), x.fst • x.snd) '' s ×ˢ t = s • t

theorem set.mem_vadd {α : Type u_2} {β : Type u_3} [has_vadd α β] {s : set α} {t : set β} {b : β} :

b ∈ s +ᵥ t ↔ ∃ (x : α) (y : β), x ∈ s ∧ y ∈ t ∧ x +ᵥ y = b

theorem set.mem_smul {α : Type u_2} {β : Type u_3} [has_smul α β] {s : set α} {t : set β} {b : β} :

b ∈ s • t ↔ ∃ (x : α) (y : β), x ∈ s ∧ y ∈ t ∧ x • y = b

theorem set.vadd_mem_vadd {α : Type u_2} {β : Type u_3} [has_vadd α β] {s : set α} {t : set β} {a : α} {b : β} :

a ∈ s → b ∈ t → a +ᵥ b ∈ s +ᵥ t

theorem set.smul_mem_smul {α : Type u_2} {β : Type u_3} [has_smul α β] {s : set α} {t : set β} {a : α} {b : β} :

a ∈ s → b ∈ t → a • b ∈ s • t

@[simp]

theorem set.empty_vadd {α : Type u_2} {β : Type u_3} [has_vadd α β] {t : set β} :

∅ +ᵥ t = ∅

@[simp]

theorem set.empty_smul {α : Type u_2} {β : Type u_3} [has_smul α β] {t : set β} :

∅ • t = ∅

@[simp]

theorem set.smul_empty {α : Type u_2} {β : Type u_3} [has_smul α β] {s : set α} :

s • ∅ = ∅

@[simp]

theorem set.vadd_empty {α : Type u_2} {β : Type u_3} [has_vadd α β] {s : set α} :

s +ᵥ ∅ = ∅

@[simp]

theorem set.vadd_eq_empty {α : Type u_2} {β : Type u_3} [has_vadd α β] {s : set α} {t : set β} :

s +ᵥ t = ∅ ↔ s = ∅ ∨ t = ∅

@[simp]

theorem set.smul_eq_empty {α : Type u_2} {β : Type u_3} [has_smul α β] {s : set α} {t : set β} :

s • t = ∅ ↔ s = ∅ ∨ t = ∅

@[simp]

theorem set.smul_nonempty {α : Type u_2} {β : Type u_3} [has_smul α β] {s : set α} {t : set β} :

(s • t).nonempty ↔ s.nonempty ∧ t.nonempty

@[simp]

theorem set.vadd_nonempty {α : Type u_2} {β : Type u_3} [has_vadd α β] {s : set α} {t : set β} :

(s +ᵥ t).nonempty ↔ s.nonempty ∧ t.nonempty

theorem set.nonempty.smul {α : Type u_2} {β : Type u_3} [has_smul α β] {s : set α} {t : set β} :

s.nonempty → t.nonempty → (s • t).nonempty

theorem set.nonempty.vadd {α : Type u_2} {β : Type u_3} [has_vadd α β] {s : set α} {t : set β} :

s.nonempty → t.nonempty → (s +ᵥ t).nonempty

theorem set.nonempty.of_smul_left {α : Type u_2} {β : Type u_3} [has_smul α β] {s : set α} {t : set β} :

(s • t).nonempty → s.nonempty

theorem set.nonempty.of_vadd_left {α : Type u_2} {β : Type u_3} [has_vadd α β] {s : set α} {t : set β} :

(s +ᵥ t).nonempty → s.nonempty

theorem set.nonempty.of_vadd_right {α : Type u_2} {β : Type u_3} [has_vadd α β] {s : set α} {t : set β} :

(s +ᵥ t).nonempty → t.nonempty

theorem set.nonempty.of_smul_right {α : Type u_2} {β : Type u_3} [has_smul α β] {s : set α} {t : set β} :

(s • t).nonempty → t.nonempty

@[simp]

theorem set.vadd_singleton {α : Type u_2} {β : Type u_3} [has_vadd α β] {s : set α} {b : β} :

s +ᵥ {b} = (λ (_x : α), _x +ᵥ b) '' s

@[simp]

theorem set.smul_singleton {α : Type u_2} {β : Type u_3} [has_smul α β] {s : set α} {b : β} :

s • {b} = (λ (_x : α), _x • b) '' s

@[simp]

theorem set.singleton_smul {α : Type u_2} {β : Type u_3} [has_smul α β] {t : set β} {a : α} :

{a} • t = a • t

@[simp]

theorem set.singleton_vadd {α : Type u_2} {β : Type u_3} [has_vadd α β] {t : set β} {a : α} :

{a} +ᵥ t = a +ᵥ t

@[simp]

theorem set.singleton_vadd_singleton {α : Type u_2} {β : Type u_3} [has_vadd α β] {a : α} {b : β} :

{a} +ᵥ {b} = {a +ᵥ b}

@[simp]

theorem set.singleton_smul_singleton {α : Type u_2} {β : Type u_3} [has_smul α β] {a : α} {b : β} :

{a} • {b} = {a • b}

theorem set.smul_subset_smul {α : Type u_2} {β : Type u_3} [has_smul α β] {s₁ s₂ : set α} {t₁ t₂ : set β} :

s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ • t₁ ⊆ s₂ • t₂

theorem set.vadd_subset_vadd {α : Type u_2} {β : Type u_3} [has_vadd α β] {s₁ s₂ : set α} {t₁ t₂ : set β} :

s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ +ᵥ t₁ ⊆ s₂ +ᵥ t₂

theorem set.vadd_subset_vadd_left {α : Type u_2} {β : Type u_3} [has_vadd α β] {s : set α} {t₁ t₂ : set β} :

t₁ ⊆ t₂ → s +ᵥ t₁ ⊆ s +ᵥ t₂

theorem set.smul_subset_smul_left {α : Type u_2} {β : Type u_3} [has_smul α β] {s : set α} {t₁ t₂ : set β} :

t₁ ⊆ t₂ → s • t₁ ⊆ s • t₂

theorem set.vadd_subset_vadd_right {α : Type u_2} {β : Type u_3} [has_vadd α β] {s₁ s₂ : set α} {t : set β} :

s₁ ⊆ s₂ → s₁ +ᵥ t ⊆ s₂ +ᵥ t

theorem set.smul_subset_smul_right {α : Type u_2} {β : Type u_3} [has_smul α β] {s₁ s₂ : set α} {t : set β} :

s₁ ⊆ s₂ → s₁ • t ⊆ s₂ • t

theorem set.vadd_subset_iff {α : Type u_2} {β : Type u_3} [has_vadd α β] {s : set α} {t u : set β} :

s +ᵥ t ⊆ u ↔ ∀ (a : α), a ∈ s → ∀ (b : β), b ∈ t → a +ᵥ b ∈ u

theorem set.smul_subset_iff {α : Type u_2} {β : Type u_3} [has_smul α β] {s : set α} {t u : set β} :

s • t ⊆ u ↔ ∀ (a : α), a ∈ s → ∀ (b : β), b ∈ t → a • b ∈ u

theorem set.union_smul {α : Type u_2} {β : Type u_3} [has_smul α β] {s₁ s₂ : set α} {t : set β} :

(s₁ ∪ s₂) • t = s₁ • t ∪ s₂ • t

theorem set.union_vadd {α : Type u_2} {β : Type u_3} [has_vadd α β] {s₁ s₂ : set α} {t : set β} :

s₁ ∪ s₂ +ᵥ t = s₁ +ᵥ t ∪ (s₂ +ᵥ t)

theorem set.smul_union {α : Type u_2} {β : Type u_3} [has_smul α β] {s : set α} {t₁ t₂ : set β} :

s • (t₁ ∪ t₂) = s • t₁ ∪ s • t₂

theorem set.vadd_union {α : Type u_2} {β : Type u_3} [has_vadd α β] {s : set α} {t₁ t₂ : set β} :

s +ᵥ (t₁ ∪ t₂) = s +ᵥ t₁ ∪ (s +ᵥ t₂)

theorem set.inter_vadd_subset {α : Type u_2} {β : Type u_3} [has_vadd α β] {s₁ s₂ : set α} {t : set β} :

s₁ ∩ s₂ +ᵥ t ⊆ (s₁ +ᵥ t) ∩ (s₂ +ᵥ t)

theorem set.inter_smul_subset {α : Type u_2} {β : Type u_3} [has_smul α β] {s₁ s₂ : set α} {t : set β} :

(s₁ ∩ s₂) • t ⊆ s₁ • t ∩ s₂ • t

theorem set.vadd_inter_subset {α : Type u_2} {β : Type u_3} [has_vadd α β] {s : set α} {t₁ t₂ : set β} :

s +ᵥ t₁ ∩ t₂ ⊆ (s +ᵥ t₁) ∩ (s +ᵥ t₂)

theorem set.smul_inter_subset {α : Type u_2} {β : Type u_3} [has_smul α β] {s : set α} {t₁ t₂ : set β} :

s • (t₁ ∩ t₂) ⊆ s • t₁ ∩ s • t₂

theorem set.Union_smul_left_image {α : Type u_2} {β : Type u_3} [has_smul α β] {s : set α} {t : set β} :

(⋃ (a : α) (H : a ∈ s), a • t) = s • t

theorem set.Union_vadd_left_image {α : Type u_2} {β : Type u_3} [has_vadd α β] {s : set α} {t : set β} :

(⋃ (a : α) (H : a ∈ s), a +ᵥ t) = s +ᵥ t

theorem set.Union_smul_right_image {α : Type u_2} {β : Type u_3} [has_smul α β] {s : set α} {t : set β} :

(⋃ (a : β) (H : a ∈ t), (λ (_x : α), _x • a) '' s) = s • t

theorem set.Union_vadd_right_image {α : Type u_2} {β : Type u_3} [has_vadd α β] {s : set α} {t : set β} :

(⋃ (a : β) (H : a ∈ t), (λ (_x : α), _x +ᵥ a) '' s) = s +ᵥ t

theorem set.Union_smul {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [has_smul α β] (s : ι → set α) (t : set β) :

(⋃ (i : ι), s i) • t = ⋃ (i : ι), s i • t

theorem set.Union_vadd {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [has_vadd α β] (s : ι → set α) (t : set β) :

(⋃ (i : ι), s i) +ᵥ t = ⋃ (i : ι), s i +ᵥ t

theorem set.smul_Union {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [has_smul α β] (s : set α) (t : ι → set β) :

(s • ⋃ (i : ι), t i) = ⋃ (i : ι), s • t i

theorem set.vadd_Union {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [has_vadd α β] (s : set α) (t : ι → set β) :

(s +ᵥ ⋃ (i : ι), t i) = ⋃ (i : ι), s +ᵥ t i

theorem set.Union₂_smul {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_6} [has_smul α β] (s : Π (i : ι), κ i → set α) (t : set β) :

(⋃ (i : ι) (j : κ i), s i j) • t = ⋃ (i : ι) (j : κ i), s i j • t

theorem set.Union₂_vadd {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_6} [has_vadd α β] (s : Π (i : ι), κ i → set α) (t : set β) :

(⋃ (i : ι) (j : κ i), s i j) +ᵥ t = ⋃ (i : ι) (j : κ i), s i j +ᵥ t

theorem set.vadd_Union₂ {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_6} [has_vadd α β] (s : set α) (t : Π (i : ι), κ i → set β) :

(s +ᵥ ⋃ (i : ι) (j : κ i), t i j) = ⋃ (i : ι) (j : κ i), s +ᵥ t i j

theorem set.smul_Union₂ {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_6} [has_smul α β] (s : set α) (t : Π (i : ι), κ i → set β) :

(s • ⋃ (i : ι) (j : κ i), t i j) = ⋃ (i : ι) (j : κ i), s • t i j

theorem set.Inter_vadd_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [has_vadd α β] (s : ι → set α) (t : set β) :

(⋂ (i : ι), s i) +ᵥ t ⊆ ⋂ (i : ι), s i +ᵥ t

theorem set.Inter_smul_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [has_smul α β] (s : ι → set α) (t : set β) :

(⋂ (i : ι), s i) • t ⊆ ⋂ (i : ι), s i • t

theorem set.vadd_Inter_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [has_vadd α β] (s : set α) (t : ι → set β) :

(s +ᵥ ⋂ (i : ι), t i) ⊆ ⋂ (i : ι), s +ᵥ t i

theorem set.smul_Inter_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [has_smul α β] (s : set α) (t : ι → set β) :

(s • ⋂ (i : ι), t i) ⊆ ⋂ (i : ι), s • t i

theorem set.Inter₂_vadd_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_6} [has_vadd α β] (s : Π (i : ι), κ i → set α) (t : set β) :

(⋂ (i : ι) (j : κ i), s i j) +ᵥ t ⊆ ⋂ (i : ι) (j : κ i), s i j +ᵥ t

theorem set.Inter₂_smul_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_6} [has_smul α β] (s : Π (i : ι), κ i → set α) (t : set β) :

(⋂ (i : ι) (j : κ i), s i j) • t ⊆ ⋂ (i : ι) (j : κ i), s i j • t

theorem set.vadd_Inter₂_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_6} [has_vadd α β] (s : set α) (t : Π (i : ι), κ i → set β) :

(s +ᵥ ⋂ (i : ι) (j : κ i), t i j) ⊆ ⋂ (i : ι) (j : κ i), s +ᵥ t i j

theorem set.smul_Inter₂_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_6} [has_smul α β] (s : set α) (t : Π (i : ι), κ i → set β) :

(s • ⋂ (i : ι) (j : κ i), t i j) ⊆ ⋂ (i : ι) (j : κ i), s • t i j

theorem set.finite.smul {α : Type u_2} {β : Type u_3} [has_smul α β] {s : set α} {t : set β} :

s.finite → t.finite → (s • t).finite

theorem set.finite.vadd {α : Type u_2} {β : Type u_3} [has_vadd α β] {s : set α} {t : set β} :

s.finite → t.finite → (s +ᵥ t).finite

@[simp]

theorem set.bUnion_smul_set {α : Type u_2} {β : Type u_3} [has_smul α β] (s : set α) (t : set β) :

(⋃ (a : α) (H : a ∈ s), a • t) = s • t

@[simp]

theorem set.bUnion_vadd_set {α : Type u_2} {β : Type u_3} [has_vadd α β] (s : set α) (t : set β) :

(⋃ (a : α) (H : a ∈ s), a +ᵥ t) = s +ᵥ t

@[simp]

theorem set.image_vadd {α : Type u_2} {β : Type u_3} [has_vadd α β] {t : set β} {a : α} :

(λ (x : β), a +ᵥ x) '' t = a +ᵥ t

@[simp]

theorem set.image_smul {α : Type u_2} {β : Type u_3} [has_smul α β] {t : set β} {a : α} :

(λ (x : β), a • x) '' t = a • t

theorem set.mem_vadd_set {α : Type u_2} {β : Type u_3} [has_vadd α β] {t : set β} {a : α} {x : β} :

x ∈ a +ᵥ t ↔ ∃ (y : β), y ∈ t ∧ a +ᵥ y = x

theorem set.mem_smul_set {α : Type u_2} {β : Type u_3} [has_smul α β] {t : set β} {a : α} {x : β} :

x ∈ a • t ↔ ∃ (y : β), y ∈ t ∧ a • y = x

theorem set.smul_mem_smul_set {α : Type u_2} {β : Type u_3} [has_smul α β] {s : set β} {a : α} {b : β} :

b ∈ s → a • b ∈ a • s

theorem set.vadd_mem_vadd_set {α : Type u_2} {β : Type u_3} [has_vadd α β] {s : set β} {a : α} {b : β} :

b ∈ s → a +ᵥ b ∈ a +ᵥ s

@[simp]

theorem set.smul_set_empty {α : Type u_2} {β : Type u_3} [has_smul α β] {a : α} :

a • ∅ = ∅

@[simp]

theorem set.vadd_set_empty {α : Type u_2} {β : Type u_3} [has_vadd α β] {a : α} :

a +ᵥ ∅ = ∅

@[simp]

theorem set.smul_set_eq_empty {α : Type u_2} {β : Type u_3} [has_smul α β] {s : set β} {a : α} :

a • s = ∅ ↔ s = ∅

@[simp]

theorem set.vadd_set_eq_empty {α : Type u_2} {β : Type u_3} [has_vadd α β] {s : set β} {a : α} :

a +ᵥ s = ∅ ↔ s = ∅

@[simp]

theorem set.smul_set_nonempty {α : Type u_2} {β : Type u_3} [has_smul α β] {s : set β} {a : α} :

(a • s).nonempty ↔ s.nonempty

@[simp]

theorem set.vadd_set_nonempty {α : Type u_2} {β : Type u_3} [has_vadd α β] {s : set β} {a : α} :

(a +ᵥ s).nonempty ↔ s.nonempty

@[simp]

theorem set.vadd_set_singleton {α : Type u_2} {β : Type u_3} [has_vadd α β] {a : α} {b : β} :

a +ᵥ {b} = {a +ᵥ b}

@[simp]

theorem set.smul_set_singleton {α : Type u_2} {β : Type u_3} [has_smul α β] {a : α} {b : β} :

a • {b} = {a • b}

theorem set.vadd_set_mono {α : Type u_2} {β : Type u_3} [has_vadd α β] {s t : set β} {a : α} :

s ⊆ t → a +ᵥ s ⊆ a +ᵥ t

theorem set.smul_set_mono {α : Type u_2} {β : Type u_3} [has_smul α β] {s t : set β} {a : α} :

s ⊆ t → a • s ⊆ a • t

theorem set.vadd_set_subset_iff {α : Type u_2} {β : Type u_3} [has_vadd α β] {s t : set β} {a : α} :

a +ᵥ s ⊆ t ↔ ∀ ⦃b : β⦄, b ∈ s → a +ᵥ b ∈ t

theorem set.smul_set_subset_iff {α : Type u_2} {β : Type u_3} [has_smul α β] {s t : set β} {a : α} :

a • s ⊆ t ↔ ∀ ⦃b : β⦄, b ∈ s → a • b ∈ t

theorem set.vadd_set_union {α : Type u_2} {β : Type u_3} [has_vadd α β] {t₁ t₂ : set β} {a : α} :

a +ᵥ (t₁ ∪ t₂) = a +ᵥ t₁ ∪ (a +ᵥ t₂)

theorem set.smul_set_union {α : Type u_2} {β : Type u_3} [has_smul α β] {t₁ t₂ : set β} {a : α} :

a • (t₁ ∪ t₂) = a • t₁ ∪ a • t₂

theorem set.smul_set_inter_subset {α : Type u_2} {β : Type u_3} [has_smul α β] {t₁ t₂ : set β} {a : α} :

a • (t₁ ∩ t₂) ⊆ a • t₁ ∩ a • t₂

theorem set.vadd_set_inter_subset {α : Type u_2} {β : Type u_3} [has_vadd α β] {t₁ t₂ : set β} {a : α} :

a +ᵥ t₁ ∩ t₂ ⊆ (a +ᵥ t₁) ∩ (a +ᵥ t₂)

theorem set.vadd_set_Union {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [has_vadd α β] (a : α) (s : ι → set β) :

(a +ᵥ ⋃ (i : ι), s i) = ⋃ (i : ι), a +ᵥ s i

theorem set.smul_set_Union {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [has_smul α β] (a : α) (s : ι → set β) :

(a • ⋃ (i : ι), s i) = ⋃ (i : ι), a • s i

theorem set.smul_set_Union₂ {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_6} [has_smul α β] (a : α) (s : Π (i : ι), κ i → set β) :

(a • ⋃ (i : ι) (j : κ i), s i j) = ⋃ (i : ι) (j : κ i), a • s i j

theorem set.vadd_set_Union₂ {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_6} [has_vadd α β] (a : α) (s : Π (i : ι), κ i → set β) :

(a +ᵥ ⋃ (i : ι) (j : κ i), s i j) = ⋃ (i : ι) (j : κ i), a +ᵥ s i j

theorem set.vadd_set_Inter_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [has_vadd α β] (a : α) (t : ι → set β) :

(a +ᵥ ⋂ (i : ι), t i) ⊆ ⋂ (i : ι), a +ᵥ t i

theorem set.smul_set_Inter_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [has_smul α β] (a : α) (t : ι → set β) :

(a • ⋂ (i : ι), t i) ⊆ ⋂ (i : ι), a • t i

theorem set.vadd_set_Inter₂_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_6} [has_vadd α β] (a : α) (t : Π (i : ι), κ i → set β) :

(a +ᵥ ⋂ (i : ι) (j : κ i), t i j) ⊆ ⋂ (i : ι) (j : κ i), a +ᵥ t i j

theorem set.smul_set_Inter₂_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_6} [has_smul α β] (a : α) (t : Π (i : ι), κ i → set β) :

(a • ⋂ (i : ι) (j : κ i), t i j) ⊆ ⋂ (i : ι) (j : κ i), a • t i j

theorem set.nonempty.vadd_set {α : Type u_2} {β : Type u_3} [has_vadd α β] {s : set β} {a : α} :

s.nonempty → (a +ᵥ s).nonempty

theorem set.nonempty.smul_set {α : Type u_2} {β : Type u_3} [has_smul α β] {s : set β} {a : α} :

s.nonempty → (a • s).nonempty

theorem set.finite.vadd_set {α : Type u_2} {β : Type u_3} [has_vadd α β] {s : set β} {a : α} :

s.finite → (a +ᵥ s).finite

theorem set.finite.smul_set {α : Type u_2} {β : Type u_3} [has_smul α β] {s : set β} {a : α} :

s.finite → (a • s).finite

theorem set.vadd_set_inter {α : Type u_2} {β : Type u_3} {a : α} [add_group α] [add_action α β] {s t : set β} :

a +ᵥ s ∩ t = (a +ᵥ s) ∩ (a +ᵥ t)

theorem set.smul_set_inter {α : Type u_2} {β : Type u_3} {a : α} [group α] [mul_action α β] {s t : set β} :

a • (s ∩ t) = a • s ∩ a • t

theorem set.smul_set_inter₀ {α : Type u_2} {β : Type u_3} {a : α} [group_with_zero α] [mul_action α β] {s t : set β} (ha : a ≠ 0) :

a • (s ∩ t) = a • s ∩ a • t

@[simp]

theorem set.smul_set_univ {α : Type u_2} {β : Type u_3} [group α] [mul_action α β] {a : α} :

a • set.univ = set.univ

@[simp]

theorem set.vadd_set_univ {α : Type u_2} {β : Type u_3} [add_group α] [add_action α β] {a : α} :

a +ᵥ set.univ = set.univ

@[simp]

theorem set.vadd_univ {α : Type u_2} {β : Type u_3} [add_group α] [add_action α β] {s : set α} (hs : s.nonempty) :

s +ᵥ set.univ = set.univ

@[simp]

theorem set.smul_univ {α : Type u_2} {β : Type u_3} [group α] [mul_action α β] {s : set α} (hs : s.nonempty) :

s • set.univ = set.univ

theorem set.range_vadd_range {α : Type u_2} {β : Type u_3} {ι : Type u_1} {κ : Type u_4} [has_vadd α β] (b : ι → α) (c : κ → β) :

set.range b +ᵥ set.range c = set.range (λ (p : ι × κ), b p.fst +ᵥ c p.snd)

theorem set.range_smul_range {α : Type u_2} {β : Type u_3} {ι : Type u_1} {κ : Type u_4} [has_smul α β] (b : ι → α) (c : κ → β) :

set.range b • set.range c = set.range (λ (p : ι × κ), b p.fst • c p.snd)

theorem set.smul_set_range {α : Type u_2} {β : Type u_3} {a : α} [has_smul α β] {ι : Sort u_1} {f : ι → β} :

a • set.range f = set.range (λ (i : ι), a • f i)

theorem set.vadd_set_range {α : Type u_2} {β : Type u_3} {a : α} [has_vadd α β] {ι : Sort u_1} {f : ι → β} :

a +ᵥ set.range f = set.range (λ (i : ι), a +ᵥ f i)

@[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 γ)

@[protected, instance]

def set.smul_comm_class_set {α : Type u_2} {β : Type u_3} {γ : Type u_4} [has_smul α γ] [has_smul β γ] [smul_comm_class α β γ] :

smul_comm_class α β (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_smul α γ] [has_smul β γ] [smul_comm_class α β γ] :

smul_comm_class α (set β) (set γ)

@[protected, instance]

def set.smul_comm_class_set'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [has_smul α γ] [has_smul β γ] [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.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_smul α γ] [has_smul β γ] [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_smul α β] [has_smul α γ] [has_smul β γ] [is_scalar_tower α β γ] :

is_scalar_tower α β (set γ)

@[protected, instance]

def set.vadd_assoc_class {α : Type u_2} {β : Type u_3} {γ : Type u_4} [has_vadd α β] [has_vadd α γ] [has_vadd β γ] [vadd_assoc_class α β γ] :

vadd_assoc_class α β (set γ)

@[protected, instance]

def set.vadd_assoc_class' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [has_vadd α β] [has_vadd α γ] [has_vadd β γ] [vadd_assoc_class α β γ] :

vadd_assoc_class α (set β) (set γ)

@[protected, instance]

def set.is_scalar_tower' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [has_smul α β] [has_smul α γ] [has_smul β γ] [is_scalar_tower α β γ] :

is_scalar_tower α (set β) (set γ)

@[protected, instance]

def set.vadd_assoc_class'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [has_vadd α β] [has_vadd α γ] [has_vadd β γ] [vadd_assoc_class α β γ] :

vadd_assoc_class (set α) (set β) (set γ)

@[protected, instance]

def set.is_scalar_tower'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [has_smul α β] [has_smul α γ] [has_smul β γ] [is_scalar_tower α β γ] :

is_scalar_tower (set α) (set β) (set γ)

@[protected, instance]

def set.is_central_scalar {α : Type u_2} {β : Type u_3} [has_smul α β] [has_smul αᵐᵒᵖ β] [is_central_scalar α β] :

is_central_scalar α (set β)

@[protected]

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_smul := set.has_smul mul_action.to_has_smul, one_smul := _, mul_smul := _}

@[protected]

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]

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]

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

set.mul_action_set = {to_has_smul := set.has_smul_set mul_action.to_has_smul, one_smul := _, mul_smul := _}

@[protected]

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

set.distrib_mul_action_set = {to_mul_action := set.mul_action_set distrib_mul_action.to_mul_action, smul_add := _, smul_zero := _}

@[protected]

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

set.mul_distrib_mul_action_set = {to_mul_action := set.mul_action_set mul_distrib_mul_action.to_mul_action, smul_mul := _, smul_one := _}

@[protected, instance]

def set.no_zero_smul_divisors {α : Type u_2} {β : Type u_3} [has_zero α] [has_zero β] [has_smul α β] [no_zero_smul_divisors α β] :

no_zero_smul_divisors (set α) (set β)

@[protected, instance]

def set.no_zero_smul_divisors_set {α : Type u_2} {β : Type u_3} [has_zero α] [has_zero β] [has_smul α β] [no_zero_smul_divisors α β] :

no_zero_smul_divisors α (set β)

@[protected, instance]

def set.no_zero_divisors {α : Type u_2} [has_zero α] [has_mul α] [no_zero_divisors α] :

no_zero_divisors (set α)

@[protected, instance]

def set.has_vsub {α : Type u_2} {β : Type u_3} [has_vsub α β] :

has_vsub (set α) (set β)

Equations

set.has_vsub = {vsub := set.image2 has_vsub.vsub}

@[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

theorem set.image_vsub_prod {α : Type u_2} {β : Type u_3} [has_vsub α β] {s t : set β} :

(λ (x : β × β), x.fst -ᵥ x.snd) '' s ×ˢ t = s -ᵥ t

theorem set.mem_vsub {α : Type u_2} {β : Type u_3} [has_vsub α β] {s t : set β} {a : α} :

a ∈ s -ᵥ t ↔ ∃ (x y : β), x ∈ s ∧ y ∈ t ∧ x -ᵥ y = a

theorem set.vsub_mem_vsub {α : Type u_2} {β : Type u_3} [has_vsub α β] {s t : set β} {b c : β} (hb : b ∈ s) (hc : c ∈ t) :

b -ᵥ c ∈ s -ᵥ t

@[simp]

theorem set.empty_vsub {α : Type u_2} {β : Type u_3} [has_vsub α β] (t : set β) :

∅ -ᵥ t = ∅

@[simp]

theorem set.vsub_empty {α : Type u_2} {β : Type u_3} [has_vsub α β] (s : set β) :

s -ᵥ ∅ = ∅

@[simp]

theorem set.vsub_eq_empty {α : Type u_2} {β : Type u_3} [has_vsub α β] {s t : set β} :

s -ᵥ t = ∅ ↔ s = ∅ ∨ t = ∅

@[simp]

theorem set.vsub_nonempty {α : Type u_2} {β : Type u_3} [has_vsub α β] {s t : set β} :

(s -ᵥ t).nonempty ↔ s.nonempty ∧ t.nonempty

theorem set.nonempty.vsub {α : Type u_2} {β : Type u_3} [has_vsub α β] {s t : set β} :

s.nonempty → t.nonempty → (s -ᵥ t).nonempty

theorem set.nonempty.of_vsub_left {α : Type u_2} {β : Type u_3} [has_vsub α β] {s t : set β} :

(s -ᵥ t).nonempty → s.nonempty

theorem set.nonempty.of_vsub_right {α : Type u_2} {β : Type u_3} [has_vsub α β] {s t : set β} :

(s -ᵥ t).nonempty → t.nonempty

@[simp]

theorem set.vsub_singleton {α : Type u_2} {β : Type u_3} [has_vsub α β] (s : set β) (b : β) :

s -ᵥ {b} = (λ (_x : β), _x -ᵥ b) '' s

@[simp]

theorem set.singleton_vsub {α : Type u_2} {β : Type u_3} [has_vsub α β] (t : set β) (b : β) :

{b} -ᵥ t = has_vsub.vsub b '' t

@[simp]

theorem set.singleton_vsub_singleton {α : Type u_2} {β : Type u_3} [has_vsub α β] {b c : β} :

{b} -ᵥ {c} = {b -ᵥ c}

theorem set.vsub_subset_vsub {α : Type u_2} {β : Type u_3} [has_vsub α β] {s₁ s₂ t₁ t₂ : set β} :

s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ -ᵥ t₁ ⊆ s₂ -ᵥ t₂

theorem set.vsub_subset_vsub_left {α : Type u_2} {β : Type u_3} [has_vsub α β] {s t₁ t₂ : set β} :

t₁ ⊆ t₂ → s -ᵥ t₁ ⊆ s -ᵥ t₂

theorem set.vsub_subset_vsub_right {α : Type u_2} {β : Type u_3} [has_vsub α β] {s₁ s₂ t : set β} :

s₁ ⊆ s₂ → s₁ -ᵥ t ⊆ s₂ -ᵥ t

theorem set.vsub_subset_iff {α : Type u_2} {β : Type u_3} [has_vsub α β] {s t : set β} {u : set α} :

s -ᵥ t ⊆ u ↔ ∀ (x : β), x ∈ s → ∀ (y : β), y ∈ t → x -ᵥ y ∈ u

theorem set.vsub_self_mono {α : Type u_2} {β : Type u_3} [has_vsub α β] {s t : set β} (h : s ⊆ t) :

s -ᵥ s ⊆ t -ᵥ t

theorem set.union_vsub {α : Type u_2} {β : Type u_3} [has_vsub α β] {s₁ s₂ t : set β} :

s₁ ∪ s₂ -ᵥ t = s₁ -ᵥ t ∪ (s₂ -ᵥ t)

theorem set.vsub_union {α : Type u_2} {β : Type u_3} [has_vsub α β] {s t₁ t₂ : set β} :

s -ᵥ (t₁ ∪ t₂) = s -ᵥ t₁ ∪ (s -ᵥ t₂)

theorem set.inter_vsub_subset {α : Type u_2} {β : Type u_3} [has_vsub α β] {s₁ s₂ t : set β} :

s₁ ∩ s₂ -ᵥ t ⊆ (s₁ -ᵥ t) ∩ (s₂ -ᵥ t)

theorem set.vsub_inter_subset {α : Type u_2} {β : Type u_3} [has_vsub α β] {s t₁ t₂ : set β} :

s -ᵥ t₁ ∩ t₂ ⊆ (s -ᵥ t₁) ∩ (s -ᵥ 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

theorem set.Union_vsub_right_image {α : Type u_2} {β : Type u_3} [has_vsub α β] {s t : set β} :

(⋃ (a : β) (H : a ∈ t), (λ (_x : β), _x -ᵥ a) '' s) = s -ᵥ t

theorem set.Union_vsub {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [has_vsub α β] (s : ι → set β) (t : set β) :

(⋃ (i : ι), s i) -ᵥ t = ⋃ (i : ι), s i -ᵥ t

theorem set.vsub_Union {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [has_vsub α β] (s : set β) (t : ι → set β) :

(s -ᵥ ⋃ (i : ι), t i) = ⋃ (i : ι), s -ᵥ t i

theorem set.Union₂_vsub {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_6} [has_vsub α β] (s : Π (i : ι), κ i → set β) (t : set β) :

(⋃ (i : ι) (j : κ i), s i j) -ᵥ t = ⋃ (i : ι) (j : κ i), s i j -ᵥ t

theorem set.vsub_Union₂ {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_6} [has_vsub α β] (s : set β) (t : Π (i : ι), κ i → set β) :

(s -ᵥ ⋃ (i : ι) (j : κ i), t i j) = ⋃ (i : ι) (j : κ i), s -ᵥ t i j

theorem set.Inter_vsub_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [has_vsub α β] (s : ι → set β) (t : set β) :

(⋂ (i : ι), s i) -ᵥ t ⊆ ⋂ (i : ι), s i -ᵥ t

theorem set.vsub_Inter_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [has_vsub α β] (s : set β) (t : ι → set β) :

(s -ᵥ ⋂ (i : ι), t i) ⊆ ⋂ (i : ι), s -ᵥ t i

theorem set.Inter₂_vsub_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_6} [has_vsub α β] (s : Π (i : ι), κ i → set β) (t : set β) :

(⋂ (i : ι) (j : κ i), s i j) -ᵥ t ⊆ ⋂ (i : ι) (j : κ i), s i j -ᵥ t

theorem set.vsub_Inter₂_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_6} [has_vsub α β] (s : set β) (t : Π (i : ι), κ i → set β) :

(s -ᵥ ⋂ (i : ι) (j : κ i), t i j) ⊆ ⋂ (i : ι) (j : κ i), s -ᵥ t i j

theorem set.finite.vsub {α : Type u_2} {β : Type u_3} [has_vsub α β] {s t : set β} (hs : s.finite) (ht : t.finite) :

(s -ᵥ t).finite

Note that we have neither smul_with_zero α (set β) nor smul_with_zero (set α) (set β) because 0 * ∅ ≠ 0.

theorem set.smul_zero_subset {α : Type u_2} {β : Type u_3} [has_zero α] [has_zero β] [smul_with_zero α β] (s : set α) :

s • 0 ⊆ 0

theorem set.zero_smul_subset {α : Type u_2} {β : Type u_3} [has_zero α] [has_zero β] [smul_with_zero α β] (t : set β) :

0 • t ⊆ 0

theorem set.nonempty.smul_zero {α : Type u_2} {β : Type u_3} [has_zero α] [has_zero β] [smul_with_zero α β] {s : set α} (hs : s.nonempty) :

s • 0 = 0

theorem set.nonempty.zero_smul {α : Type u_2} {β : Type u_3} [has_zero α] [has_zero β] [smul_with_zero α β] {t : set β} (ht : t.nonempty) :

0 • t = 0

theorem set.zero_smul_set {α : Type u_2} {β : Type u_3} [has_zero α] [has_zero β] [smul_with_zero α β] {s : set β} (h : s.nonempty) :

0 • s = 0

A nonempty set is scaled by zero to the singleton set containing 0.

theorem set.zero_smul_set_subset {α : Type u_2} {β : Type u_3} [has_zero α] [has_zero β] [smul_with_zero α β] (s : set β) :

0 • s ⊆ 0

theorem set.subsingleton_zero_smul_set {α : Type u_2} {β : Type u_3} [has_zero α] [has_zero β] [smul_with_zero α β] (s : set β) :

(0 • s).subsingleton

theorem set.zero_mem_smul_set {α : Type u_2} {β : Type u_3} [has_zero α] [has_zero β] [smul_with_zero α β] {t : set β} {a : α} (h : 0 ∈ t) :

0 ∈ a • t

theorem set.zero_mem_smul_iff {α : Type u_2} {β : Type u_3} [has_zero α] [has_zero β] [smul_with_zero α β] {s : set α} {t : set β} [no_zero_smul_divisors α β] :

0 ∈ s • t ↔ 0 ∈ s ∧ t.nonempty ∨ 0 ∈ t ∧ s.nonempty

theorem set.zero_mem_smul_set_iff {α : Type u_2} {β : Type u_3} [has_zero α] [has_zero β] [smul_with_zero α β] {t : set β} [no_zero_smul_divisors α β] {a : α} (ha : a ≠ 0) :

0 ∈ a • t ↔ 0 ∈ t

theorem set.pairwise_disjoint_smul_iff {α : Type u_2} [left_cancel_semigroup α] {s t : set α} :

s.pairwise_disjoint (λ (_x : α), _x • t) ↔ set.inj_on (λ (p : α × α), p.fst * p.snd) (s ×ˢ t)

theorem set.pairwise_disjoint_vadd_iff {α : Type u_2} [add_left_cancel_semigroup α] {s t : set α} :

s.pairwise_disjoint (λ (_x : α), _x +ᵥ t) ↔ set.inj_on (λ (p : α × α), p.fst + p.snd) (s ×ˢ t)

@[simp]

theorem set.vadd_mem_vadd_set_iff {α : Type u_2} {β : Type u_3} [add_group α] [add_action α β] {s : set β} {a : α} {x : β} :

a +ᵥ x ∈ a +ᵥ s ↔ x ∈ s

@[simp]

theorem set.smul_mem_smul_set_iff {α : Type u_2} {β : Type u_3} [group α] [mul_action α β] {s : set β} {a : α} {x : β} :

a • x ∈ a • s ↔ x ∈ s

theorem set.mem_smul_set_iff_inv_smul_mem {α : Type u_2} {β : Type u_3} [group α] [mul_action α β] {A : set β} {a : α} {x : β} :

x ∈ a • A ↔ a⁻¹ • x ∈ A

theorem set.mem_vadd_set_iff_neg_vadd_mem {α : Type u_2} {β : Type u_3} [add_group α] [add_action α β] {A : set β} {a : α} {x : β} :

x ∈ a +ᵥ A ↔ -a +ᵥ x ∈ A

theorem set.mem_inv_smul_set_iff {α : Type u_2} {β : Type u_3} [group α] [mul_action α β] {A : set β} {a : α} {x : β} :

x ∈ a⁻¹ • A ↔ a • x ∈ A

theorem set.mem_neg_vadd_set_iff {α : Type u_2} {β : Type u_3} [add_group α] [add_action α β] {A : set β} {a : α} {x : β} :

x ∈ -a +ᵥ A ↔ a +ᵥ x ∈ A

theorem set.preimage_smul {α : Type u_2} {β : Type u_3} [group α] [mul_action α β] (a : α) (t : set β) :

(λ (x : β), a • x) ⁻¹' t = a⁻¹ • t

theorem set.preimage_vadd {α : Type u_2} {β : Type u_3} [add_group α] [add_action α β] (a : α) (t : set β) :

(λ (x : β), a +ᵥ x) ⁻¹' t = -a +ᵥ t

theorem set.preimage_smul_inv {α : Type u_2} {β : Type u_3} [group α] [mul_action α β] (a : α) (t : set β) :

(λ (x : β), a⁻¹ • x) ⁻¹' t = a • t

theorem set.preimage_vadd_neg {α : Type u_2} {β : Type u_3} [add_group α] [add_action α β] (a : α) (t : set β) :

(λ (x : β), -a +ᵥ x) ⁻¹' t = a +ᵥ t

@[simp]

theorem set.set_vadd_subset_set_vadd_iff {α : Type u_2} {β : Type u_3} [add_group α] [add_action α β] {A B : set β} {a : α} :

a +ᵥ A ⊆ a +ᵥ B ↔ A ⊆ B

@[simp]

theorem set.set_smul_subset_set_smul_iff {α : Type u_2} {β : Type u_3} [group α] [mul_action α β] {A B : set β} {a : α} :

a • A ⊆ a • B ↔ A ⊆ B

theorem set.set_smul_subset_iff {α : Type u_2} {β : Type u_3} [group α] [mul_action α β] {A B : set β} {a : α} :

a • A ⊆ B ↔ A ⊆ a⁻¹ • B

theorem set.set_vadd_subset_iff {α : Type u_2} {β : Type u_3} [add_group α] [add_action α β] {A B : set β} {a : α} :

a +ᵥ A ⊆ B ↔ A ⊆ -a +ᵥ B

theorem set.subset_set_smul_iff {α : Type u_2} {β : Type u_3} [group α] [mul_action α β] {A B : set β} {a : α} :

A ⊆ a • B ↔ a⁻¹ • A ⊆ B

theorem set.subset_set_vadd_iff {α : Type u_2} {β : Type u_3} [add_group α] [add_action α β] {A B : set β} {a : α} :

A ⊆ a +ᵥ B ↔ -a +ᵥ A ⊆ B

@[simp]

theorem set.smul_mem_smul_set_iff₀ {α : Type u_2} {β : Type u_3} [group_with_zero α] [mul_action α β] {a : α} (ha : a ≠ 0) (A : set β) (x : β) :

a • x ∈ a • A ↔ x ∈ A

theorem set.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 : β) :

x ∈ a • A ↔ a⁻¹ • x ∈ A

theorem set.mem_inv_smul_set_iff₀ {α : Type u_2} {β : Type u_3} [group_with_zero α] [mul_action α β] {a : α} (ha : a ≠ 0) (A : set β) (x : β) :

x ∈ a⁻¹ • A ↔ a • x ∈ A

theorem set.preimage_smul₀ {α : Type u_2} {β : Type u_3} [group_with_zero α] [mul_action α β] {a : α} (ha : a ≠ 0) (t : set β) :

(λ (x : β), a • x) ⁻¹' t = a⁻¹ • t

theorem set.preimage_smul_inv₀ {α : Type u_2} {β : Type u_3} [group_with_zero α] [mul_action α β] {a : α} (ha : a ≠ 0) (t : set β) :

(λ (x : β), a⁻¹ • x) ⁻¹' t = a • t

@[simp]

theorem set.set_smul_subset_set_smul_iff₀ {α : Type u_2} {β : Type u_3} [group_with_zero α] [mul_action α β] {a : α} (ha : a ≠ 0) {A B : set β} :

a • A ⊆ a • B ↔ A ⊆ B

theorem set.set_smul_subset_iff₀ {α : Type u_2} {β : Type u_3} [group_with_zero α] [mul_action α β] {a : α} (ha : a ≠ 0) {A B : set β} :

a • A ⊆ B ↔ A ⊆ a⁻¹ • B

theorem set.subset_set_smul_iff₀ {α : Type u_2} {β : Type u_3} [group_with_zero α] [mul_action α β] {a : α} (ha : a ≠ 0) {A B : set β} :

A ⊆ a • B ↔ a⁻¹ • A ⊆ B

theorem set.smul_univ₀ {α : Type u_2} {β : Type u_3} [group_with_zero α] [mul_action α β] {s : set α} (hs : ¬s ⊆ 0) :

s • set.univ = set.univ

theorem set.smul_set_univ₀ {α : Type u_2} {β : Type u_3} [group_with_zero α] [mul_action α β] {a : α} (ha : a ≠ 0) :

a • set.univ = set.univ

@[simp]

theorem set.smul_set_neg {α : Type u_2} {β : Type u_3} [monoid α] [add_group β] [distrib_mul_action α β] (a : α) (t : set β) :

a • -t = -(a • t)

@[protected, simp]

theorem set.smul_neg {α : Type u_2} {β : Type u_3} [monoid α] [add_group β] [distrib_mul_action α β] (s : set α) (t : set β) :

s • -t = -(s • t)

@[simp]

theorem set.neg_smul_set {α : Type u_2} {β : Type u_3} [ring α] [add_comm_group β] [module α β] (a : α) (t : set β) :

-a • t = -(a • t)

@[protected, simp]

theorem set.neg_smul {α : Type u_2} {β : Type u_3} [ring α] [add_comm_group β] [module α β] (s : set α) (t : set β) :

-s • t = -(s • t)

Miscellaneous #

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 submonoid.mul_subset {M : Type u_5} [monoid M] {s t : set M} {S : submonoid M} (hs : s ⊆ ↑S) (ht : t ⊆ ↑S) :

s * t ⊆ ↑S

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) :

s + 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 add_submonoid.coe_add_self_eq {M : Type u_5} [add_monoid M] (s : add_submonoid M) :

↑s + ↑s = ↑s

theorem submonoid.coe_mul_self_eq {M : Type u_5} [monoid M] (s : submonoid M) :

↑s * ↑s = ↑s

theorem add_submonoid.closure_add_le {M : Type u_5} [add_monoid M] (S T : set M) :

add_submonoid.closure (S + T) ≤ add_submonoid.closure S ⊔ add_submonoid.closure T

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 add_submonoid.sup_eq_closure {M : Type u_5} [add_monoid M] (H K : add_submonoid M) :

H ⊔ K = add_submonoid.closure (↑H + ↑K)

theorem submonoid.sup_eq_closure {M : Type u_5} [monoid M] (H K : submonoid M) :

H ⊔ K = submonoid.closure (↑H * ↑K)

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) :

∃ (n : ℕ), r ^ n • x ∈ submonoid.closure (r • s)

theorem add_submonoid.nsmul_vadd_mem_closure_vadd {M : Type u_5} [add_monoid M] {N : Type u_1} [add_comm_monoid N] [add_action M N] [vadd_assoc_class M N N] (r : M) (s : set N) {x : N} (hx : x ∈ add_submonoid.closure s) :

∃ (n : ℕ), n • r +ᵥ x ∈ add_submonoid.closure (r +ᵥ s)

theorem group.card_pow_eq_card_pow_card_univ_aux {f : ℕ → ℕ} (h1 : monotone f) {B : ℕ} (h2 : ∀ (n : ℕ), f n ≤ B) (h3 : ∀ (n : ℕ), f n = f (n + 1) → f (n + 1) = f (n + 2)) (k : ℕ) :

B ≤ k → f k = f B

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)

theorem set.is_pwo.mul {α : Type u_2} {s t : set α} [ordered_cancel_comm_monoid α] (hs : s.is_pwo) (ht : t.is_pwo) :

(s * t).is_pwo

theorem set.is_pwo.add {α : Type u_2} {s t : set α} [ordered_cancel_add_comm_monoid α] (hs : s.is_pwo) (ht : t.is_pwo) :

(s + t).is_pwo

theorem set.is_wf.add {α : Type u_2} {s t : set α} [linear_ordered_cancel_add_comm_monoid α] (hs : s.is_wf) (ht : t.is_wf) :

(s + t).is_wf

theorem set.is_wf.mul {α : Type u_2} {s t : set α} [linear_ordered_cancel_comm_monoid α] (hs : s.is_wf) (ht : t.is_wf) :

(s * t).is_wf

theorem set.is_wf.min_add {α : Type u_2} {s t : set α} [linear_ordered_cancel_add_comm_monoid α] (hs : s.is_wf) (ht : t.is_wf) (hsn : s.nonempty) (htn : t.nonempty) :

_.min _ = hs.min hsn + ht.min htn

theorem set.is_wf.min_mul {α : Type u_2} {s t : set α} [linear_ordered_cancel_comm_monoid α] (hs : s.is_wf) (ht : t.is_wf) (hsn : s.nonempty) (htn : t.nonempty) :

_.min _ = hs.min hsn * ht.min htn

Multiplication antidiagonal #

def set.mul_antidiagonal {α : Type u_2} [has_mul α] (s t : set α) (a : α) :

set (α × α)

set.mul_antidiagonal s t a is the set of all pairs of an element in s and an element in t that multiply to a.

Equations

s.mul_antidiagonal t a = {x : α × α | x.fst ∈ s ∧ x.snd ∈ t ∧ x.fst * x.snd = a}

def set.add_antidiagonal {α : Type u_2} [has_add α] (s t : set α) (a : α) :

set (α × α)

set.add_antidiagonal s t a is the set of all pairs of an element in s and an element in t that add to a.

Equations

s.add_antidiagonal t a = {x : α × α | x.fst ∈ s ∧ x.snd ∈ t ∧ x.fst + x.snd = a}

@[simp]

theorem set.mem_add_antidiagonal {α : Type u_2} [has_add α] {s t : set α} {a : α} {x : α × α} :

x ∈ s.add_antidiagonal t a ↔ x.fst ∈ s ∧ x.snd ∈ t ∧ x.fst + x.snd = a

@[simp]

theorem set.mem_mul_antidiagonal {α : Type u_2} [has_mul α] {s t : set α} {a : α} {x : α × α} :

x ∈ s.mul_antidiagonal t a ↔ x.fst ∈ s ∧ x.snd ∈ t ∧ x.fst * x.snd = a

theorem set.mul_antidiagonal_mono_left {α : Type u_2} [has_mul α] {s₁ s₂ t : set α} {a : α} (h : s₁ ⊆ s₂) :

s₁.mul_antidiagonal t a ⊆ s₂.mul_antidiagonal t a

theorem set.add_antidiagonal_mono_left {α : Type u_2} [has_add α] {s₁ s₂ t : set α} {a : α} (h : s₁ ⊆ s₂) :

s₁.add_antidiagonal t a ⊆ s₂.add_antidiagonal t a

theorem set.mul_antidiagonal_mono_right {α : Type u_2} [has_mul α] {s t₁ t₂ : set α} {a : α} (h : t₁ ⊆ t₂) :

s.mul_antidiagonal t₁ a ⊆ s.mul_antidiagonal t₂ a

theorem set.add_antidiagonal_mono_right {α : Type u_2} [has_add α] {s t₁ t₂ : set α} {a : α} (h : t₁ ⊆ t₂) :

s.add_antidiagonal t₁ a ⊆ s.add_antidiagonal t₂ a

@[simp]

theorem set.swap_mem_mul_antidiagonal {α : Type u_2} [comm_semigroup α] {s t : set α} {a : α} {x : α × α} :

x.swap ∈ s.mul_antidiagonal t a ↔ x ∈ t.mul_antidiagonal s a

@[simp]

theorem set.swap_mem_add_antidiagonal {α : Type u_2} [add_comm_semigroup α] {s t : set α} {a : α} {x : α × α} :

x.swap ∈ s.add_antidiagonal t a ↔ x ∈ t.add_antidiagonal s a

theorem set.mul_antidiagonal.fst_eq_fst_iff_snd_eq_snd {α : Type u_2} [cancel_comm_monoid α] {s t : set α} {a : α} {x y : ↥(s.mul_antidiagonal t a)} :

↑x.fst = ↑y.fst ↔ ↑x.snd = ↑y.snd

theorem set.add_antidiagonal.fst_eq_fst_iff_snd_eq_snd {α : Type u_2} [add_cancel_comm_monoid α] {s t : set α} {a : α} {x y : ↥(s.add_antidiagonal t a)} :

↑x.fst = ↑y.fst ↔ ↑x.snd = ↑y.snd

theorem set.add_antidiagonal.eq_of_fst_eq_fst {α : Type u_2} [add_cancel_comm_monoid α] {s t : set α} {a : α} {x y : ↥(s.add_antidiagonal t a)} (h : ↑x.fst = ↑y.fst) :

x = y

theorem set.mul_antidiagonal.eq_of_fst_eq_fst {α : Type u_2} [cancel_comm_monoid α] {s t : set α} {a : α} {x y : ↥(s.mul_antidiagonal t a)} (h : ↑x.fst = ↑y.fst) :

x = y

theorem set.add_antidiagonal.eq_of_snd_eq_snd {α : Type u_2} [add_cancel_comm_monoid α] {s t : set α} {a : α} {x y : ↥(s.add_antidiagonal t a)} (h : ↑x.snd = ↑y.snd) :

x = y

theorem set.mul_antidiagonal.eq_of_snd_eq_snd {α : Type u_2} [cancel_comm_monoid α] {s t : set α} {a : α} {x y : ↥(s.mul_antidiagonal t a)} (h : ↑x.snd = ↑y.snd) :

x = y

theorem set.mul_antidiagonal.eq_of_fst_le_fst_of_snd_le_snd {α : Type u_2} [ordered_cancel_comm_monoid α] (s t : set α) (a : α) {x y : ↥(s.mul_antidiagonal t a)} (h₁ : ↑x.fst ≤ ↑y.fst) (h₂ : ↑x.snd ≤ ↑y.snd) :

x = y

theorem set.add_antidiagonal.eq_of_fst_le_fst_of_snd_le_snd {α : Type u_2} [ordered_cancel_add_comm_monoid α] (s t : set α) (a : α) {x y : ↥(s.add_antidiagonal t a)} (h₁ : ↑x.fst ≤ ↑y.fst) (h₂ : ↑x.snd ≤ ↑y.snd) :

x = y

theorem set.mul_antidiagonal.finite_of_is_pwo {α : Type u_2} [ordered_cancel_comm_monoid α] {s t : set α} (hs : s.is_pwo) (ht : t.is_pwo) (a : α) :

(s.mul_antidiagonal t a).finite

theorem set.add_antidiagonal.finite_of_is_pwo {α : Type u_2} [ordered_cancel_add_comm_monoid α] {s t : set α} (hs : s.is_pwo) (ht : t.is_pwo) (a : α) :

(s.add_antidiagonal t a).finite

theorem set.add_antidiagonal.finite_of_is_wf {α : Type u_2} [linear_ordered_cancel_add_comm_monoid α] {s t : set α} (hs : s.is_wf) (ht : t.is_wf) (a : α) :

(s.add_antidiagonal t a).finite

theorem set.mul_antidiagonal.finite_of_is_wf {α : Type u_2} [linear_ordered_cancel_comm_monoid α] {s t : set α} (hs : s.is_wf) (ht : t.is_wf) (a : α) :

(s.mul_antidiagonal t a).finite

noncomputable def finset.mul_antidiagonal {α : Type u_2} [ordered_cancel_comm_monoid α] {s t : set α} (hs : s.is_pwo) (ht : t.is_pwo) (a : α) :

finset (α × α)

finset.mul_antidiagonal_of_is_wf hs ht a is the set of all pairs of an element in s and an element in t that multiply to a, but its construction requires proofs that s and t are well-ordered.

Equations

finset.mul_antidiagonal hs ht a = _.to_finset

noncomputable def finset.add_antidiagonal {α : Type u_2} [ordered_cancel_add_comm_monoid α] {s t : set α} (hs : s.is_pwo) (ht : t.is_pwo) (a : α) :

finset (α × α)

finset.add_antidiagonal_of_is_wf hs ht a is the set of all pairs of an element in s and an element in t that add to a, but its construction requires proofs that s and t are well-ordered.

Equations

finset.add_antidiagonal hs ht a = _.to_finset

@[simp]

theorem finset.mem_mul_antidiagonal {α : Type u_2} [ordered_cancel_comm_monoid α] {s t : set α} {hs : s.is_pwo} {ht : t.is_pwo} {a : α} {x : α × α} :

x ∈ finset.mul_antidiagonal hs ht a ↔ x.fst ∈ s ∧ x.snd ∈ t ∧ x.fst * x.snd = a

@[simp]

theorem finset.mem_add_antidiagonal {α : Type u_2} [ordered_cancel_add_comm_monoid α] {s t : set α} {hs : s.is_pwo} {ht : t.is_pwo} {a : α} {x : α × α} :

x ∈ finset.add_antidiagonal hs ht a ↔ x.fst ∈ s ∧ x.snd ∈ t ∧ x.fst + x.snd = a

theorem finset.mul_antidiagonal_mono_left {α : Type u_2} [ordered_cancel_comm_monoid α] {s t : set α} {hs : s.is_pwo} {ht : t.is_pwo} {a : α} {u : set α} {hu : u.is_pwo} (h : u ⊆ s) :

finset.mul_antidiagonal hu ht a ⊆ finset.mul_antidiagonal hs ht a

theorem finset.add_antidiagonal_mono_left {α : Type u_2} [ordered_cancel_add_comm_monoid α] {s t : set α} {hs : s.is_pwo} {ht : t.is_pwo} {a : α} {u : set α} {hu : u.is_pwo} (h : u ⊆ s) :

finset.add_antidiagonal hu ht a ⊆ finset.add_antidiagonal hs ht a

theorem finset.mul_antidiagonal_mono_right {α : Type u_2} [ordered_cancel_comm_monoid α] {s t : set α} {hs : s.is_pwo} {ht : t.is_pwo} {a : α} {u : set α} {hu : u.is_pwo} (h : u ⊆ t) :

finset.mul_antidiagonal hs hu a ⊆ finset.mul_antidiagonal hs ht a

theorem finset.add_antidiagonal_mono_right {α : Type u_2} [ordered_cancel_add_comm_monoid α] {s t : set α} {hs : s.is_pwo} {ht : t.is_pwo} {a : α} {u : set α} {hu : u.is_pwo} (h : u ⊆ t) :

finset.add_antidiagonal hs hu a ⊆ finset.add_antidiagonal hs ht a

@[simp]

theorem finset.swap_mem_mul_antidiagonal {α : Type u_2} [ordered_cancel_comm_monoid α] {s t : set α} {hs : s.is_pwo} {ht : t.is_pwo} {a : α} {x : α × α} :

x.swap ∈ finset.mul_antidiagonal hs ht a ↔ x ∈ finset.mul_antidiagonal ht hs a

@[simp]

theorem finset.swap_mem_add_antidiagonal {α : Type u_2} [ordered_cancel_add_comm_monoid α] {s t : set α} {hs : s.is_pwo} {ht : t.is_pwo} {a : α} {x : α × α} :

x.swap ∈ finset.add_antidiagonal hs ht a ↔ x ∈ finset.add_antidiagonal ht hs a

theorem finset.support_add_antidiagonal_subset_add {α : Type u_2} [ordered_cancel_add_comm_monoid α] {s t : set α} {hs : s.is_pwo} {ht : t.is_pwo} :

{a : α | (finset.add_antidiagonal hs ht a).nonempty} ⊆ s + t

theorem finset.support_mul_antidiagonal_subset_mul {α : Type u_2} [ordered_cancel_comm_monoid α] {s t : set α} {hs : s.is_pwo} {ht : t.is_pwo} :

{a : α | (finset.mul_antidiagonal hs ht a).nonempty} ⊆ s * t

theorem finset.is_pwo_support_add_antidiagonal {α : Type u_2} [ordered_cancel_add_comm_monoid α] {s t : set α} {hs : s.is_pwo} {ht : t.is_pwo} :

{a : α | (finset.add_antidiagonal hs ht a).nonempty}.is_pwo

theorem finset.is_pwo_support_mul_antidiagonal {α : Type u_2} [ordered_cancel_comm_monoid α] {s t : set α} {hs : s.is_pwo} {ht : t.is_pwo} :

{a : α | (finset.mul_antidiagonal hs ht a).nonempty}.is_pwo

theorem finset.add_antidiagonal_min_add_min {α : Type u_1} [linear_ordered_cancel_add_comm_monoid α] {s t : set α} (hs : s.is_wf) (ht : t.is_wf) (hns : s.nonempty) (hnt : t.nonempty) :

finset.add_antidiagonal _ _ (hs.min hns + ht.min hnt) = {(hs.min hns, ht.min hnt)}

theorem finset.mul_antidiagonal_min_mul_min {α : Type u_1} [linear_ordered_cancel_comm_monoid α] {s t : set α} (hs : s.is_wf) (ht : t.is_wf) (hns : s.nonempty) (hnt : t.nonempty) :

finset.mul_antidiagonal _ _ (hs.min hns * ht.min hnt) = {(hs.min hns, ht.min hnt)}