# mathlib3documentation

data.set.pointwise.basic

# Pointwise operations of sets #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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`.

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`.

## 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

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 α] :

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

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

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

Equations
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 α] :
(set α)

The singleton operation as a `zero_hom`.

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

The singleton operation as a `one_hom`.

Equations
@[simp]
theorem set.coe_singleton_zero_hom {α : Type u_2} [has_zero α] :
@[simp]
theorem set.coe_singleton_one_hom {α : Type u_2} [has_one α] :

### Set negation/inversion #

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

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
@[protected]
def set.has_inv {α : Type u_2} [has_inv α] :

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
@[simp]
theorem set.mem_inv {α : Type u_2} [has_inv α] {s : set α} {a : α} :
@[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 α} :
@[simp]
theorem set.neg_preimage {α : Type u_2} [has_neg α] {s : set α} :
= -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 α] :
@[simp]
theorem set.inv_univ {α : Type u_2} [has_inv α] :
@[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 α} :
@[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 α} :
@[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 α} :
theorem set.inv_mem_inv {α : Type u_2} {s : set α} {a : α} :
theorem set.neg_mem_neg {α : Type u_2} {s : set α} {a : α} :
-a -s a s
@[simp]
theorem set.nonempty_neg {α : Type u_2} {s : set α} :
@[simp]
theorem set.nonempty_inv {α : Type u_2} {s : set α} :
theorem set.nonempty.inv {α : Type u_2} {s : set α} (h : s.nonempty) :
theorem set.nonempty.neg {α : Type u_2} {s : set α} (h : s.nonempty) :
@[simp]
theorem set.image_inv {α : Type u_2} {s : set α} :
@[simp]
theorem set.image_neg {α : Type u_2} {s : set α} :
= -s
@[protected, simp, instance]
def set.has_involutive_neg {α : Type u_2}  :
Equations
@[protected, simp, instance]
def set.has_involutive_inv {α : Type u_2}  :
Equations
@[simp]
theorem set.neg_subset_neg {α : Type u_2} {s t : set α} :
-s -t s t
@[simp]
theorem set.inv_subset_inv {α : Type u_2} {s t : set α} :
theorem set.inv_subset {α : Type u_2} {s t : set α} :
theorem set.neg_subset {α : Type u_2} {s t : set α} :
-s t s -t
@[simp]
theorem set.inv_singleton {α : Type u_2} (a : α) :
{a}⁻¹ = {a⁻¹}
@[simp]
theorem set.neg_singleton {α : Type u_2} (a : α) :
-{a} = {-a}
@[simp]
theorem set.inv_insert {α : Type u_2} (a : α) (s : set α) :
@[simp]
theorem set.neg_insert {α : Type u_2} (a : α) (s : set α) :
= (-s)
theorem set.inv_range {α : Type u_2} {ι : Sort u_1} {f : ι α} :
(set.range f)⁻¹ = set.range (λ (i : ι), (f i)⁻¹)
theorem set.neg_range {α : Type u_2} {ι : Sort u_1} {f : ι α} :
= set.range (λ (i : ι), -f i)
theorem set.image_op_neg {α : Type u_2} {s : set α} :
theorem set.image_op_inv {α : Type u_2} {s : set α} :

### Set addition/multiplication #

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

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

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

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

Equations
@[simp]
theorem set.image2_mul {α : Type u_2} [has_mul α] {s t : set α} :
= s * t
@[simp]
theorem set.image2_add {α : Type u_2} [has_add α] {s t : set α} :
= 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
@[simp]
theorem set.add_nonempty {α : Type u_2} [has_add α] {s t : set α} :
(s + t).nonempty
theorem set.nonempty.add {α : Type u_2} [has_add α] {s t : set α} :
theorem set.nonempty.mul {α : Type u_2} [has_mul α] {s t : set α} :
theorem set.nonempty.of_add_left {α : Type u_2} [has_add α] {s t : set α} :
theorem set.nonempty.of_mul_left {α : Type u_2} [has_mul α] {s t : set α} :
theorem set.nonempty.of_add_right {α : Type u_2} [has_add α] {s t : set α} :
theorem set.nonempty.of_mul_right {α : Type u_2} [has_mul α] {s t : set α} :
@[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 =
@[simp]
theorem set.singleton_mul {α : Type u_2} [has_mul α] {t : set α} {a : α} :
{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.inter_mul_union_subset_union {α : Type u_2} [has_mul α] {s₁ s₂ t₁ t₂ : set α} :
s₁ s₂ * (t₁ t₂) s₁ * t₁ s₂ * t₂
theorem set.inter_add_union_subset_union {α : Type u_2} [has_add α] {s₁ s₂ t₁ t₂ : set α} :
s₁ s₂ + (t₁ t₂) s₁ + t₁ (s₂ + t₂)
theorem set.union_mul_inter_subset_union {α : Type u_2} [has_mul α] {s₁ s₂ t₁ t₂ : set α} :
(s₁ s₂) * (t₁ t₂) s₁ * t₁ s₂ * t₂
theorem set.union_add_inter_subset_union {α : Type u_2} [has_add α] {s₁ s₂ t₁ t₂ : set α} :
s₁ 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), '' t) = s * t
theorem set.Union_add_left_image {α : Type u_2} [has_add α] {s t : set α} :
( (a : α) (H : a s), '' 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
def set.singleton_mul_hom {α : Type u_2} [has_mul α] :
α →ₙ* set α

The singleton operation as a `mul_hom`.

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

The singleton operation as an `add_hom`.

Equations
@[simp]
theorem set.coe_singleton_add_hom {α : Type u_2} [has_add α] :
@[simp]
theorem set.coe_singleton_mul_hom {α : Type u_2} [has_mul α] :
@[simp]
theorem set.singleton_add_hom_apply {α : Type u_2} [has_add α] (a : α) :
@[simp]
theorem set.singleton_mul_hom_apply {α : Type u_2} [has_mul α] (a : α) :
@[simp]
theorem set.image_op_add {α : Type u_2} [has_add α] {s t : set α} :
@[simp]
theorem set.image_op_mul {α : Type u_2} [has_mul α] {s t : set α} :

### Set subtraction/division #

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

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

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

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

Equations
@[simp]
theorem set.image2_sub {α : Type u_2} [has_sub α] {s t : set α} :
= s - t
@[simp]
theorem set.image2_div {α : Type u_2} [has_div α] {s t : set α} :
= 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
@[simp]
theorem set.sub_nonempty {α : Type u_2} [has_sub α] {s t : set α} :
(s - t).nonempty
theorem set.nonempty.div {α : Type u_2} [has_div α] {s t : set α} :
theorem set.nonempty.sub {α : Type u_2} [has_sub α] {s t : set α} :
theorem set.nonempty.of_sub_left {α : Type u_2} [has_sub α] {s t : set α} :
theorem set.nonempty.of_div_left {α : Type u_2} [has_div α] {s t : set α} :
theorem set.nonempty.of_div_right {α : Type u_2} [has_div α] {s t : set α} :
theorem set.nonempty.of_sub_right {α : Type u_2} [has_sub α] {s t : set α} :
@[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 =
@[simp]
theorem set.singleton_sub {α : Type u_2} [has_sub α] {t : set α} {a : α} :
{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.inter_div_union_subset_union {α : Type u_2} [has_div α] {s₁ s₂ t₁ t₂ : set α} :
s₁ s₂ / (t₁ t₂) s₁ / t₁ s₂ / t₂
theorem set.inter_sub_union_subset_union {α : Type u_2} [has_sub α] {s₁ s₂ t₁ t₂ : set α} :
s₁ s₂ - (t₁ t₂) s₁ - t₁ (s₂ - t₂)
theorem set.union_div_inter_subset_union {α : Type u_2} [has_div α] {s₁ s₂ t₁ t₂ : set α} :
(s₁ s₂) / (t₁ t₂) s₁ / t₁ s₂ / t₂
theorem set.union_sub_inter_subset_union {α : Type u_2} [has_sub α] {s₁ s₂ t₁ t₂ : set α} :
s₁ 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), '' t) = s - t
theorem set.Union_div_left_image {α : Type u_2} [has_div α] {s t : set α} :
( (a : α) (H : a s), '' 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 α] :
(set α)

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

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

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

Equations
@[protected]
def set.has_zsmul {α : Type u_2} [has_zero α] [has_add α] [has_neg α] :
(set α)

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

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

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

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

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

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

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

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

`set α` is an `add_comm_semigroup` under pointwise operations if `α` is.

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

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

Equations
theorem set.inter_mul_union_subset {α : Type u_2} {s t : set α} :
s t * (s t) s * t
theorem set.inter_add_union_subset {α : Type u_2} {s t : set α} :
s t + (s t) s + t
theorem set.union_mul_inter_subset {α : Type u_2} {s t : set α} :
(s t) * (s t) s * t
theorem set.union_add_inter_subset {α : Type u_2} {s t : set α} :
s t + s t s + t
@[protected]
def set.add_zero_class {α : Type u_2}  :

`set α` is an `add_zero_class` under pointwise operations if `α` is.

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

`set α` is a `mul_one_class` under pointwise operations if `α` is.

Equations
theorem set.subset_mul_left {α : Type u_2} (s : set α) {t : set α} (ht : 1 t) :
s s * t
theorem set.subset_add_left {α : Type u_2} (s : set α) {t : set α} (ht : 0 t) :
s s + t
theorem set.subset_add_right {α : Type u_2} {s : set α} (t : set α) (hs : 0 s) :
t s + t
theorem set.subset_mul_right {α : Type u_2} {s : set α} (t : set α) (hs : 1 s) :
t s * t
def set.singleton_monoid_hom {α : Type u_2}  :
α →* set α

The singleton operation as a `monoid_hom`.

Equations
def set.singleton_add_monoid_hom {α : Type u_2}  :
α →+ set α

The singleton operation as an `add_monoid_hom`.

Equations
@[simp]
theorem set.coe_singleton_monoid_hom {α : Type u_2}  :
@[simp]
@[simp]
theorem set.singleton_add_monoid_hom_apply {α : Type u_2} (a : α) :
@[simp]
theorem set.singleton_monoid_hom_apply {α : Type u_2} (a : α) :
@[protected]
def set.monoid {α : Type u_2} [monoid α] :
monoid (set α)

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

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

`set α` is an `add_monoid` under pointwise operations if `α` is.

Equations
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
@[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) :
theorem set.mul_univ_of_one_mem {α : Type u_2} [monoid α] {s : set α} (hs : 1 s) :
theorem set.add_univ_of_zero_mem {α : Type u_2} [add_monoid α] {s : set α} (hs : 0 s) :
theorem set.univ_add_of_zero_mem {α : Type u_2} [add_monoid α] {t : set α} (ht : 0 t) :
theorem set.univ_mul_of_one_mem {α : Type u_2} [monoid α] {t : set α} (ht : 1 t) :
@[simp]
theorem set.univ_add_univ {α : Type u_2} [add_monoid α] :
@[simp]
theorem set.univ_mul_univ {α : Type u_2} [monoid α] :
@[simp]
theorem set.nsmul_univ {α : Type u_1} [add_monoid α] {n : } :
n 0
@[simp]
theorem set.univ_pow {α : Type u_2} [monoid α] {n : } :
n 0
@[protected]
theorem is_unit.set {α : Type u_2} [monoid α] {a : α} :
@[protected]
theorem is_add_unit.set {α : Type u_2} [add_monoid α] {a : α} :
@[protected]
def set.comm_monoid {α : Type u_2} [comm_monoid α] :

`set α` is a `comm_monoid` under pointwise operations if `α` is.

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

`set α` is an `add_comm_monoid` under pointwise operations if `α` is.

Equations
@[protected]
theorem set.mul_eq_one_iff {α : Type u_2} {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} {s t : set α} :
s + t = 0 (a b : α), s = {a} t = {b} a + b = 0
@[protected]
def set.subtraction_monoid {α : Type u_2}  :

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

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

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

Equations
@[simp]
theorem set.is_unit_iff {α : Type u_2} {s : set α} :
(a : α), s = {a}
@[simp]
theorem set.is_add_unit_iff {α : Type u_2} {s : set α} :
(a : α), s = {a}
@[protected]
def set.division_comm_monoid {α : Type u_2}  :

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

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

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

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

`set α` has distributive negation if `α` has.

Equations

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} (s : set α) :
s * 0 0
theorem set.zero_mul_subset {α : Type u_2} (s : set α) :
0 * s 0
theorem set.nonempty.mul_zero {α : Type u_2} {s : set α} (hs : s.nonempty) :
s * 0 = 0
theorem set.nonempty.zero_mul {α : Type u_2} {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 ¬ t
@[simp]
theorem set.zero_mem_sub_iff {α : Type u_2} [add_group α] {s t : set α} :
0 s - t ¬ t
theorem set.not_zero_mem_sub_iff {α : Type u_2} [add_group α] {s t : set α} :
0 s - t t
theorem set.not_one_mem_div_iff {α : Type u_2} [group α] {s t : set α} :
1 s / t t
theorem disjoint.one_not_mem_div_set {α : Type u_2} [group α] {s t : set α} :
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 α} :
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 : α) :
@[simp]
theorem set.is_add_unit_iff_singleton {α : Type u_2} [add_group α] {s : set α} :
(a : α), s = {a}
@[simp]
theorem set.is_unit_iff_singleton {α : Type u_2} [group α] {s : set α} :
(a : α), s = {a}
@[simp]
theorem set.image_add_left {α : Type u_2} [add_group α] {t : set α} {a : α} :
@[simp]
theorem set.image_mul_left {α : Type u_2} [group α] {t : set α} {a : α} :
=
@[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 : α} :
⁻¹' {b} = {a⁻¹ * b}
@[simp]
theorem set.preimage_add_left_singleton {α : Type u_2} [add_group α] {a b : α} :
⁻¹' {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 : α} :
= {a⁻¹}
@[simp]
theorem set.preimage_add_left_zero {α : Type u_2} [add_group α] {a : α} :
= {-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) :
@[simp]
theorem set.add_univ {α : Type u_2} [add_group α] {s : set α} (hs : s.nonempty) :
@[simp]
theorem set.univ_mul {α : Type u_2} [group α] {t : set α} (ht : t.nonempty) :
@[simp]
theorem set.univ_add {α : Type u_2} [add_group α] {t : set α} (ht : t.nonempty) :
theorem set.div_zero_subset {α : Type u_2} (s : set α) :
s / 0 0
theorem set.zero_div_subset {α : Type u_2} (s : set α) :
0 / s 0
theorem set.nonempty.div_zero {α : Type u_2} {s : set α} (hs : s.nonempty) :
s / 0 = 0
theorem set.nonempty.zero_div {α : Type u_2} {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 β] [ β] (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 β] [ β] (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 β] [ β] (m : F) {s t : set β} :
theorem set.preimage_add_preimage_subset {F : Type u_1} {α : Type u_2} {β : Type u_3} [has_add α] [has_add β] [ β] (m : F) {s t : set β} :
theorem set.image_div {F : Type u_1} {α : Type u_2} {β : Type u_3} [group α] [ β] (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 α] [ β] (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 α] [ β] (m : F) {s t : set β} :
theorem set.preimage_sub_preimage_subset {F : Type u_1} {α : Type u_2} {β : Type u_3} [add_group α] [ β] (m : F) {s t : set β} :
theorem set.bdd_above_add {α : Type u_2} {A B : set α} :
theorem set.bdd_above_mul {α : Type u_2} {A B : set α} :

### Miscellaneous #

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