Documentation

Mathlib.Algebra.Group.Pointwise.Set.Basic

Pointwise operations of sets #

This file defines pointwise algebraic operations on sets.

Main declarations #

For sets s and t and scalar a:

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 #

Tags #

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

0/1 as sets #

noncomputable def Set.zero {α : Type u_2} [Zero α] :
Zero (Set α)

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

Equations
  • Set.zero = { zero := {0} }
Instances For
    noncomputable def Set.one {α : Type u_2} [One α] :
    One (Set α)

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

    Equations
    • Set.one = { one := {1} }
    Instances For
      theorem Set.singleton_zero {α : Type u_2} [Zero α] :
      {0} = 0
      theorem Set.singleton_one {α : Type u_2} [One α] :
      {1} = 1
      @[simp]
      theorem Set.mem_zero {α : Type u_2} [Zero α] {a : α} :
      a 0 a = 0
      @[simp]
      theorem Set.mem_one {α : Type u_2} [One α] {a : α} :
      a 1 a = 1
      theorem Set.zero_mem_zero {α : Type u_2} [Zero α] :
      0 0
      theorem Set.one_mem_one {α : Type u_2} [One α] :
      1 1
      @[simp]
      theorem Set.zero_subset {α : Type u_2} [Zero α] {s : Set α} :
      0 s 0 s
      @[simp]
      theorem Set.one_subset {α : Type u_2} [One α] {s : Set α} :
      1 s 1 s
      theorem Set.zero_nonempty {α : Type u_2} [Zero α] :
      theorem Set.one_nonempty {α : Type u_2} [One α] :
      @[simp]
      theorem Set.image_zero {α : Type u_2} {β : Type u_3} [Zero α] {f : αβ} :
      f '' 0 = {f 0}
      @[simp]
      theorem Set.image_one {α : Type u_2} {β : Type u_3} [One α] {f : αβ} :
      f '' 1 = {f 1}
      theorem Set.subset_zero_iff_eq {α : Type u_2} [Zero α] {s : Set α} :
      s 0 s = s = 0
      theorem Set.subset_one_iff_eq {α : Type u_2} [One α] {s : Set α} :
      s 1 s = s = 1
      theorem Set.Nonempty.subset_zero_iff {α : Type u_2} [Zero α] {s : Set α} (h : s.Nonempty) :
      s 0 s = 0
      theorem Set.Nonempty.subset_one_iff {α : Type u_2} [One α] {s : Set α} (h : s.Nonempty) :
      s 1 s = 1
      noncomputable def Set.singletonZeroHom {α : Type u_2} [Zero α] :
      ZeroHom α (Set α)

      The singleton operation as a ZeroHom.

      Equations
      • Set.singletonZeroHom = { toFun := singleton, map_zero' := }
      Instances For
        noncomputable def Set.singletonOneHom {α : Type u_2} [One α] :
        OneHom α (Set α)

        The singleton operation as a OneHom.

        Equations
        • Set.singletonOneHom = { toFun := singleton, map_one' := }
        Instances For
          @[simp]
          theorem Set.coe_singletonZeroHom {α : Type u_2} [Zero α] :
          Set.singletonZeroHom = singleton
          @[simp]
          theorem Set.coe_singletonOneHom {α : Type u_2} [One α] :
          Set.singletonOneHom = singleton
          theorem Set.image_op_zero {α : Type u_2} [Zero α] :
          AddOpposite.op '' 0 = 0
          theorem Set.image_op_one {α : Type u_2} [One α] :
          MulOpposite.op '' 1 = 1

          Set negation/inversion #

          def Set.neg {α : Type u_2} [Neg α] :
          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
          Instances For
            def Set.inv {α : Type u_2} [Inv α] :
            Inv (Set α)

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

            Equations
            Instances For
              @[simp]
              theorem Set.mem_neg {α : Type u_2} [Neg α] {s : Set α} {a : α} :
              a -s -a s
              @[simp]
              theorem Set.mem_inv {α : Type u_2} [Inv α] {s : Set α} {a : α} :
              @[simp]
              theorem Set.neg_preimage {α : Type u_2} [Neg α] {s : Set α} :
              Neg.neg ⁻¹' s = -s
              @[simp]
              theorem Set.inv_preimage {α : Type u_2} [Inv α] {s : Set α} :
              Inv.inv ⁻¹' s = s⁻¹
              @[simp]
              theorem Set.neg_empty {α : Type u_2} [Neg α] :
              @[simp]
              theorem Set.inv_empty {α : Type u_2} [Inv α] :
              @[simp]
              theorem Set.neg_univ {α : Type u_2} [Neg α] :
              -Set.univ = Set.univ
              @[simp]
              theorem Set.inv_univ {α : Type u_2} [Inv α] :
              Set.univ⁻¹ = Set.univ
              @[simp]
              theorem Set.inter_neg {α : Type u_2} [Neg α] {s : Set α} {t : Set α} :
              -(s t) = -s -t
              @[simp]
              theorem Set.inter_inv {α : Type u_2} [Inv α] {s : Set α} {t : Set α} :
              @[simp]
              theorem Set.union_neg {α : Type u_2} [Neg α] {s : Set α} {t : Set α} :
              -(s t) = -s -t
              @[simp]
              theorem Set.union_inv {α : Type u_2} [Inv α] {s : Set α} {t : Set α} :
              @[simp]
              theorem Set.iInter_neg {α : Type u_2} {ι : Sort u_5} [Neg α] (s : ιSet α) :
              -⋂ (i : ι), s i = ⋂ (i : ι), -s i
              @[simp]
              theorem Set.iInter_inv {α : Type u_2} {ι : Sort u_5} [Inv α] (s : ιSet α) :
              (⋂ (i : ι), s i)⁻¹ = ⋂ (i : ι), (s i)⁻¹
              @[simp]
              theorem Set.sInter_neg {α : Type u_2} [Neg α] (S : Set (Set α)) :
              -⋂₀ S = sS, -s
              @[simp]
              theorem Set.sInter_inv {α : Type u_2} [Inv α] (S : Set (Set α)) :
              (⋂₀ S)⁻¹ = sS, s⁻¹
              @[simp]
              theorem Set.iUnion_neg {α : Type u_2} {ι : Sort u_5} [Neg α] (s : ιSet α) :
              -⋃ (i : ι), s i = ⋃ (i : ι), -s i
              @[simp]
              theorem Set.iUnion_inv {α : Type u_2} {ι : Sort u_5} [Inv α] (s : ιSet α) :
              (⋃ (i : ι), s i)⁻¹ = ⋃ (i : ι), (s i)⁻¹
              @[simp]
              theorem Set.sUnion_neg {α : Type u_2} [Neg α] (S : Set (Set α)) :
              -⋃₀ S = sS, -s
              @[simp]
              theorem Set.sUnion_inv {α : Type u_2} [Inv α] (S : Set (Set α)) :
              (⋃₀ S)⁻¹ = sS, s⁻¹
              @[simp]
              theorem Set.compl_neg {α : Type u_2} [Neg α] {s : Set α} :
              -s = (-s)
              @[simp]
              theorem Set.compl_inv {α : Type u_2} [Inv α] {s : Set α} :
              theorem Set.neg_mem_neg {α : Type u_2} [InvolutiveNeg α] {s : Set α} {a : α} :
              -a -s a s
              theorem Set.inv_mem_inv {α : Type u_2} [InvolutiveInv α] {s : Set α} {a : α} :
              @[simp]
              theorem Set.nonempty_neg {α : Type u_2} [InvolutiveNeg α] {s : Set α} :
              (-s).Nonempty s.Nonempty
              @[simp]
              theorem Set.nonempty_inv {α : Type u_2} [InvolutiveInv α] {s : Set α} :
              s⁻¹.Nonempty s.Nonempty
              theorem Set.Nonempty.neg {α : Type u_2} [InvolutiveNeg α] {s : Set α} (h : s.Nonempty) :
              (-s).Nonempty
              theorem Set.Nonempty.inv {α : Type u_2} [InvolutiveInv α] {s : Set α} (h : s.Nonempty) :
              s⁻¹.Nonempty
              @[simp]
              theorem Set.image_neg {α : Type u_2} [InvolutiveNeg α] {s : Set α} :
              Neg.neg '' s = -s
              @[simp]
              theorem Set.image_inv {α : Type u_2} [InvolutiveInv α] {s : Set α} :
              Inv.inv '' s = s⁻¹
              @[simp]
              theorem Set.neg_eq_empty {α : Type u_2} [InvolutiveNeg α] {s : Set α} :
              -s = s =
              @[simp]
              theorem Set.inv_eq_empty {α : Type u_2} [InvolutiveInv α] {s : Set α} :
              noncomputable instance Set.involutiveNeg {α : Type u_2} [InvolutiveNeg α] :
              Equations
              noncomputable instance Set.involutiveInv {α : Type u_2} [InvolutiveInv α] :
              Equations
              @[simp]
              theorem Set.neg_subset_neg {α : Type u_2} [InvolutiveNeg α] {s : Set α} {t : Set α} :
              -s -t s t
              @[simp]
              theorem Set.inv_subset_inv {α : Type u_2} [InvolutiveInv α] {s : Set α} {t : Set α} :
              theorem Set.neg_subset {α : Type u_2} [InvolutiveNeg α] {s : Set α} {t : Set α} :
              -s t s -t
              theorem Set.inv_subset {α : Type u_2} [InvolutiveInv α] {s : Set α} {t : Set α} :
              @[simp]
              theorem Set.neg_singleton {α : Type u_2} [InvolutiveNeg α] (a : α) :
              -{a} = {-a}
              @[simp]
              theorem Set.inv_singleton {α : Type u_2} [InvolutiveInv α] (a : α) :
              {a}⁻¹ = {a⁻¹}
              @[simp]
              theorem Set.neg_insert {α : Type u_2} [InvolutiveNeg α] (a : α) (s : Set α) :
              -insert a s = insert (-a) (-s)
              @[simp]
              theorem Set.inv_insert {α : Type u_2} [InvolutiveInv α] (a : α) (s : Set α) :
              theorem Set.neg_range {α : Type u_2} [InvolutiveNeg α] {ι : Sort u_5} {f : ια} :
              -Set.range f = Set.range fun (i : ι) => -f i
              theorem Set.inv_range {α : Type u_2} [InvolutiveInv α] {ι : Sort u_5} {f : ια} :
              (Set.range f)⁻¹ = Set.range fun (i : ι) => (f i)⁻¹
              theorem Set.image_op_neg {α : Type u_2} [InvolutiveNeg α] {s : Set α} :
              AddOpposite.op '' (-s) = -AddOpposite.op '' s
              theorem Set.image_op_inv {α : Type u_2} [InvolutiveInv α] {s : Set α} :
              MulOpposite.op '' s⁻¹ = (MulOpposite.op '' s)⁻¹

              Set addition/multiplication #

              def Set.add {α : Type u_2} [Add α] :
              Add (Set α)

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

              Equations
              Instances For
                def Set.mul {α : Type u_2} [Mul α] :
                Mul (Set α)

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

                Equations
                Instances For
                  @[simp]
                  theorem Set.image2_add {α : Type u_2} [Add α] {s : Set α} {t : Set α} :
                  Set.image2 (fun (x1 x2 : α) => x1 + x2) s t = s + t
                  @[simp]
                  theorem Set.image2_mul {α : Type u_2} [Mul α] {s : Set α} {t : Set α} :
                  Set.image2 (fun (x1 x2 : α) => x1 * x2) s t = s * t
                  theorem Set.mem_add {α : Type u_2} [Add α] {s : Set α} {t : Set α} {a : α} :
                  a s + t xs, yt, x + y = a
                  theorem Set.mem_mul {α : Type u_2} [Mul α] {s : Set α} {t : Set α} {a : α} :
                  a s * t xs, yt, x * y = a
                  theorem Set.add_mem_add {α : Type u_2} [Add α] {s : Set α} {t : Set α} {a : α} {b : α} :
                  a sb ta + b s + t
                  theorem Set.mul_mem_mul {α : Type u_2} [Mul α] {s : Set α} {t : Set α} {a : α} {b : α} :
                  a sb ta * b s * t
                  theorem Set.add_image_prod {α : Type u_2} [Add α] {s : Set α} {t : Set α} :
                  (fun (x : α × α) => x.1 + x.2) '' s ×ˢ t = s + t
                  theorem Set.image_mul_prod {α : Type u_2} [Mul α] {s : Set α} {t : Set α} :
                  (fun (x : α × α) => x.1 * x.2) '' s ×ˢ t = s * t
                  @[simp]
                  theorem Set.empty_add {α : Type u_2} [Add α] {s : Set α} :
                  @[simp]
                  theorem Set.empty_mul {α : Type u_2} [Mul α] {s : Set α} :
                  @[simp]
                  theorem Set.add_empty {α : Type u_2} [Add α] {s : Set α} :
                  @[simp]
                  theorem Set.mul_empty {α : Type u_2} [Mul α] {s : Set α} :
                  @[simp]
                  theorem Set.add_eq_empty {α : Type u_2} [Add α] {s : Set α} {t : Set α} :
                  s + t = s = t =
                  @[simp]
                  theorem Set.mul_eq_empty {α : Type u_2} [Mul α] {s : Set α} {t : Set α} :
                  s * t = s = t =
                  @[simp]
                  theorem Set.add_nonempty {α : Type u_2} [Add α] {s : Set α} {t : Set α} :
                  (s + t).Nonempty s.Nonempty t.Nonempty
                  @[simp]
                  theorem Set.mul_nonempty {α : Type u_2} [Mul α] {s : Set α} {t : Set α} :
                  (s * t).Nonempty s.Nonempty t.Nonempty
                  theorem Set.Nonempty.add {α : Type u_2} [Add α] {s : Set α} {t : Set α} :
                  s.Nonemptyt.Nonempty(s + t).Nonempty
                  theorem Set.Nonempty.mul {α : Type u_2} [Mul α] {s : Set α} {t : Set α} :
                  s.Nonemptyt.Nonempty(s * t).Nonempty
                  theorem Set.Nonempty.of_add_left {α : Type u_2} [Add α] {s : Set α} {t : Set α} :
                  (s + t).Nonemptys.Nonempty
                  theorem Set.Nonempty.of_mul_left {α : Type u_2} [Mul α] {s : Set α} {t : Set α} :
                  (s * t).Nonemptys.Nonempty
                  theorem Set.Nonempty.of_add_right {α : Type u_2} [Add α] {s : Set α} {t : Set α} :
                  (s + t).Nonemptyt.Nonempty
                  theorem Set.Nonempty.of_mul_right {α : Type u_2} [Mul α] {s : Set α} {t : Set α} :
                  (s * t).Nonemptyt.Nonempty
                  @[simp]
                  theorem Set.add_singleton {α : Type u_2} [Add α] {s : Set α} {b : α} :
                  s + {b} = (fun (x : α) => x + b) '' s
                  @[simp]
                  theorem Set.mul_singleton {α : Type u_2} [Mul α] {s : Set α} {b : α} :
                  s * {b} = (fun (x : α) => x * b) '' s
                  @[simp]
                  theorem Set.singleton_add {α : Type u_2} [Add α] {t : Set α} {a : α} :
                  {a} + t = (fun (x : α) => a + x) '' t
                  @[simp]
                  theorem Set.singleton_mul {α : Type u_2} [Mul α] {t : Set α} {a : α} :
                  {a} * t = (fun (x : α) => a * x) '' t
                  theorem Set.singleton_add_singleton {α : Type u_2} [Add α] {a : α} {b : α} :
                  {a} + {b} = {a + b}
                  theorem Set.singleton_mul_singleton {α : Type u_2} [Mul α] {a : α} {b : α} :
                  {a} * {b} = {a * b}
                  theorem Set.add_subset_add {α : Type u_2} [Add α] {s₁ : Set α} {s₂ : Set α} {t₁ : Set α} {t₂ : Set α} :
                  s₁ t₁s₂ t₂s₁ + s₂ t₁ + t₂
                  theorem Set.mul_subset_mul {α : Type u_2} [Mul α] {s₁ : Set α} {s₂ : Set α} {t₁ : Set α} {t₂ : Set α} :
                  s₁ t₁s₂ t₂s₁ * s₂ t₁ * t₂
                  theorem Set.add_subset_add_left {α : Type u_2} [Add α] {s : Set α} {t₁ : Set α} {t₂ : Set α} :
                  t₁ t₂s + t₁ s + t₂
                  theorem Set.mul_subset_mul_left {α : Type u_2} [Mul α] {s : Set α} {t₁ : Set α} {t₂ : Set α} :
                  t₁ t₂s * t₁ s * t₂
                  theorem Set.add_subset_add_right {α : Type u_2} [Add α] {s₁ : Set α} {s₂ : Set α} {t : Set α} :
                  s₁ s₂s₁ + t s₂ + t
                  theorem Set.mul_subset_mul_right {α : Type u_2} [Mul α] {s₁ : Set α} {s₂ : Set α} {t : Set α} :
                  s₁ s₂s₁ * t s₂ * t
                  theorem Set.add_subset_iff {α : Type u_2} [Add α] {s : Set α} {t : Set α} {u : Set α} :
                  s + t u xs, yt, x + y u
                  theorem Set.mul_subset_iff {α : Type u_2} [Mul α] {s : Set α} {t : Set α} {u : Set α} :
                  s * t u xs, yt, x * y u
                  theorem Set.union_add {α : Type u_2} [Add α] {s₁ : Set α} {s₂ : Set α} {t : Set α} :
                  s₁ s₂ + t = s₁ + t (s₂ + t)
                  theorem Set.union_mul {α : Type u_2} [Mul α] {s₁ : Set α} {s₂ : Set α} {t : Set α} :
                  (s₁ s₂) * t = s₁ * t s₂ * t
                  theorem Set.add_union {α : Type u_2} [Add α] {s : Set α} {t₁ : Set α} {t₂ : Set α} :
                  s + (t₁ t₂) = s + t₁ (s + t₂)
                  theorem Set.mul_union {α : Type u_2} [Mul α] {s : Set α} {t₁ : Set α} {t₂ : Set α} :
                  s * (t₁ t₂) = s * t₁ s * t₂
                  theorem Set.inter_add_subset {α : Type u_2} [Add α] {s₁ : Set α} {s₂ : Set α} {t : Set α} :
                  s₁ s₂ + t (s₁ + t) (s₂ + t)
                  theorem Set.inter_mul_subset {α : Type u_2} [Mul α] {s₁ : Set α} {s₂ : Set α} {t : Set α} :
                  s₁ s₂ * t s₁ * t (s₂ * t)
                  theorem Set.add_inter_subset {α : Type u_2} [Add α] {s : Set α} {t₁ : Set α} {t₂ : Set α} :
                  s + t₁ t₂ (s + t₁) (s + t₂)
                  theorem Set.mul_inter_subset {α : Type u_2} [Mul α] {s : Set α} {t₁ : Set α} {t₂ : Set α} :
                  s * (t₁ t₂) s * t₁ (s * t₂)
                  theorem Set.inter_add_union_subset_union {α : Type u_2} [Add α] {s₁ : Set α} {s₂ : Set α} {t₁ : Set α} {t₂ : Set α} :
                  s₁ s₂ + (t₁ t₂) s₁ + t₁ (s₂ + t₂)
                  theorem Set.inter_mul_union_subset_union {α : Type u_2} [Mul α] {s₁ : Set α} {s₂ : Set α} {t₁ : Set α} {t₂ : Set α} :
                  s₁ s₂ * (t₁ t₂) s₁ * t₁ s₂ * t₂
                  theorem Set.union_add_inter_subset_union {α : Type u_2} [Add α] {s₁ : Set α} {s₂ : Set α} {t₁ : Set α} {t₂ : Set α} :
                  s₁ s₂ + t₁ t₂ s₁ + t₁ (s₂ + t₂)
                  theorem Set.union_mul_inter_subset_union {α : Type u_2} [Mul α] {s₁ : Set α} {s₂ : Set α} {t₁ : Set α} {t₂ : Set α} :
                  (s₁ s₂) * (t₁ t₂) s₁ * t₁ s₂ * t₂
                  theorem Set.iUnion_add_left_image {α : Type u_2} [Add α] {s : Set α} {t : Set α} :
                  as, (fun (x : α) => a + x) '' t = s + t
                  theorem Set.iUnion_mul_left_image {α : Type u_2} [Mul α] {s : Set α} {t : Set α} :
                  as, (fun (x : α) => a * x) '' t = s * t
                  theorem Set.iUnion_add_right_image {α : Type u_2} [Add α] {s : Set α} {t : Set α} :
                  at, (fun (x : α) => x + a) '' s = s + t
                  theorem Set.iUnion_mul_right_image {α : Type u_2} [Mul α] {s : Set α} {t : Set α} :
                  at, (fun (x : α) => x * a) '' s = s * t
                  theorem Set.iUnion_add {α : Type u_2} {ι : Sort u_5} [Add α] (s : ιSet α) (t : Set α) :
                  (⋃ (i : ι), s i) + t = ⋃ (i : ι), s i + t
                  theorem Set.iUnion_mul {α : Type u_2} {ι : Sort u_5} [Mul α] (s : ιSet α) (t : Set α) :
                  (⋃ (i : ι), s i) * t = ⋃ (i : ι), s i * t
                  theorem Set.add_iUnion {α : Type u_2} {ι : Sort u_5} [Add α] (s : Set α) (t : ιSet α) :
                  s + ⋃ (i : ι), t i = ⋃ (i : ι), s + t i
                  theorem Set.mul_iUnion {α : Type u_2} {ι : Sort u_5} [Mul α] (s : Set α) (t : ιSet α) :
                  s * ⋃ (i : ι), t i = ⋃ (i : ι), s * t i
                  theorem Set.sUnion_add {α : Type u_2} [Add α] (S : Set (Set α)) (t : Set α) :
                  ⋃₀ S + t = sS, s + t
                  theorem Set.sUnion_mul {α : Type u_2} [Mul α] (S : Set (Set α)) (t : Set α) :
                  ⋃₀ S * t = sS, s * t
                  theorem Set.add_sUnion {α : Type u_2} [Add α] (s : Set α) (T : Set (Set α)) :
                  s + ⋃₀ T = tT, s + t
                  theorem Set.mul_sUnion {α : Type u_2} [Mul α] (s : Set α) (T : Set (Set α)) :
                  s * ⋃₀ T = tT, s * t
                  theorem Set.iUnion₂_add {α : Type u_2} {ι : Sort u_5} {κ : ιSort u_6} [Add α] (s : (i : ι) → κ iSet α) (t : Set α) :
                  (⋃ (i : ι), ⋃ (j : κ i), s i j) + t = ⋃ (i : ι), ⋃ (j : κ i), s i j + t
                  theorem Set.iUnion₂_mul {α : Type u_2} {ι : Sort u_5} {κ : ιSort u_6} [Mul α] (s : (i : ι) → κ iSet α) (t : Set α) :
                  (⋃ (i : ι), ⋃ (j : κ i), s i j) * t = ⋃ (i : ι), ⋃ (j : κ i), s i j * t
                  theorem Set.add_iUnion₂ {α : Type u_2} {ι : Sort u_5} {κ : ιSort u_6} [Add α] (s : Set α) (t : (i : ι) → κ iSet α) :
                  s + ⋃ (i : ι), ⋃ (j : κ i), t i j = ⋃ (i : ι), ⋃ (j : κ i), s + t i j
                  theorem Set.mul_iUnion₂ {α : Type u_2} {ι : Sort u_5} {κ : ιSort u_6} [Mul α] (s : Set α) (t : (i : ι) → κ iSet α) :
                  s * ⋃ (i : ι), ⋃ (j : κ i), t i j = ⋃ (i : ι), ⋃ (j : κ i), s * t i j
                  theorem Set.iInter_add_subset {α : Type u_2} {ι : Sort u_5} [Add α] (s : ιSet α) (t : Set α) :
                  (⋂ (i : ι), s i) + t ⋂ (i : ι), s i + t
                  theorem Set.iInter_mul_subset {α : Type u_2} {ι : Sort u_5} [Mul α] (s : ιSet α) (t : Set α) :
                  (⋂ (i : ι), s i) * t ⋂ (i : ι), s i * t
                  theorem Set.add_iInter_subset {α : Type u_2} {ι : Sort u_5} [Add α] (s : Set α) (t : ιSet α) :
                  s + ⋂ (i : ι), t i ⋂ (i : ι), s + t i
                  theorem Set.mul_iInter_subset {α : Type u_2} {ι : Sort u_5} [Mul α] (s : Set α) (t : ιSet α) :
                  s * ⋂ (i : ι), t i ⋂ (i : ι), s * t i
                  theorem Set.add_sInter_subset {α : Type u_2} [Add α] (s : Set α) (T : Set (Set α)) :
                  s + ⋂₀ T tT, s + t
                  theorem Set.mul_sInter_subset {α : Type u_2} [Mul α] (s : Set α) (T : Set (Set α)) :
                  s * ⋂₀ T tT, s * t
                  theorem Set.sInter_add_subset {α : Type u_2} [Add α] (S : Set (Set α)) (t : Set α) :
                  ⋂₀ S + t sS, s + t
                  theorem Set.sInter_mul_subset {α : Type u_2} [Mul α] (S : Set (Set α)) (t : Set α) :
                  ⋂₀ S * t sS, s * t
                  theorem Set.iInter₂_add_subset {α : Type u_2} {ι : Sort u_5} {κ : ιSort u_6} [Add α] (s : (i : ι) → κ iSet α) (t : Set α) :
                  (⋂ (i : ι), ⋂ (j : κ i), s i j) + t ⋂ (i : ι), ⋂ (j : κ i), s i j + t
                  theorem Set.iInter₂_mul_subset {α : Type u_2} {ι : Sort u_5} {κ : ιSort u_6} [Mul α] (s : (i : ι) → κ iSet α) (t : Set α) :
                  (⋂ (i : ι), ⋂ (j : κ i), s i j) * t ⋂ (i : ι), ⋂ (j : κ i), s i j * t
                  theorem Set.add_iInter₂_subset {α : Type u_2} {ι : Sort u_5} {κ : ιSort u_6} [Add α] (s : Set α) (t : (i : ι) → κ iSet α) :
                  s + ⋂ (i : ι), ⋂ (j : κ i), t i j ⋂ (i : ι), ⋂ (j : κ i), s + t i j
                  theorem Set.mul_iInter₂_subset {α : Type u_2} {ι : Sort u_5} {κ : ιSort u_6} [Mul α] (s : Set α) (t : (i : ι) → κ iSet α) :
                  s * ⋂ (i : ι), ⋂ (j : κ i), t i j ⋂ (i : ι), ⋂ (j : κ i), s * t i j
                  noncomputable def Set.singletonAddHom {α : Type u_2} [Add α] :
                  AddHom α (Set α)

                  The singleton operation as an AddHom.

                  Equations
                  • Set.singletonAddHom = { toFun := singleton, map_add' := }
                  Instances For
                    noncomputable def Set.singletonMulHom {α : Type u_2} [Mul α] :
                    α →ₙ* Set α

                    The singleton operation as a MulHom.

                    Equations
                    • Set.singletonMulHom = { toFun := singleton, map_mul' := }
                    Instances For
                      @[simp]
                      theorem Set.coe_singletonAddHom {α : Type u_2} [Add α] :
                      Set.singletonAddHom = singleton
                      @[simp]
                      theorem Set.coe_singletonMulHom {α : Type u_2} [Mul α] :
                      Set.singletonMulHom = singleton
                      @[simp]
                      theorem Set.singletonAddHom_apply {α : Type u_2} [Add α] (a : α) :
                      Set.singletonAddHom a = {a}
                      @[simp]
                      theorem Set.singletonMulHom_apply {α : Type u_2} [Mul α] (a : α) :
                      Set.singletonMulHom a = {a}
                      @[simp]
                      theorem Set.image_op_add {α : Type u_2} [Add α] {s : Set α} {t : Set α} :
                      AddOpposite.op '' (s + t) = AddOpposite.op '' t + AddOpposite.op '' s
                      @[simp]
                      theorem Set.image_op_mul {α : Type u_2} [Mul α] {s : Set α} {t : Set α} :
                      MulOpposite.op '' (s * t) = MulOpposite.op '' t * MulOpposite.op '' s

                      Set subtraction/division #

                      def Set.sub {α : Type u_2} [Sub α] :
                      Sub (Set α)

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

                      Equations
                      Instances For
                        def Set.div {α : Type u_2} [Div α] :
                        Div (Set α)

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

                        Equations
                        Instances For
                          @[simp]
                          theorem Set.image2_sub {α : Type u_2} [Sub α] {s : Set α} {t : Set α} :
                          Set.image2 Sub.sub s t = s - t
                          @[simp]
                          theorem Set.image2_div {α : Type u_2} [Div α] {s : Set α} {t : Set α} :
                          Set.image2 Div.div s t = s / t
                          theorem Set.mem_sub {α : Type u_2} [Sub α] {s : Set α} {t : Set α} {a : α} :
                          a s - t xs, yt, x - y = a
                          theorem Set.mem_div {α : Type u_2} [Div α] {s : Set α} {t : Set α} {a : α} :
                          a s / t xs, yt, x / y = a
                          theorem Set.sub_mem_sub {α : Type u_2} [Sub α] {s : Set α} {t : Set α} {a : α} {b : α} :
                          a sb ta - b s - t
                          theorem Set.div_mem_div {α : Type u_2} [Div α] {s : Set α} {t : Set α} {a : α} {b : α} :
                          a sb ta / b s / t
                          theorem Set.sub_image_prod {α : Type u_2} [Sub α] {s : Set α} {t : Set α} :
                          (fun (x : α × α) => x.1 - x.2) '' s ×ˢ t = s - t
                          theorem Set.image_div_prod {α : Type u_2} [Div α] {s : Set α} {t : Set α} :
                          (fun (x : α × α) => x.1 / x.2) '' s ×ˢ t = s / t
                          @[simp]
                          theorem Set.empty_sub {α : Type u_2} [Sub α] {s : Set α} :
                          @[simp]
                          theorem Set.empty_div {α : Type u_2} [Div α] {s : Set α} :
                          @[simp]
                          theorem Set.sub_empty {α : Type u_2} [Sub α] {s : Set α} :
                          @[simp]
                          theorem Set.div_empty {α : Type u_2} [Div α] {s : Set α} :
                          @[simp]
                          theorem Set.sub_eq_empty {α : Type u_2} [Sub α] {s : Set α} {t : Set α} :
                          s - t = s = t =
                          @[simp]
                          theorem Set.div_eq_empty {α : Type u_2} [Div α] {s : Set α} {t : Set α} :
                          s / t = s = t =
                          @[simp]
                          theorem Set.sub_nonempty {α : Type u_2} [Sub α] {s : Set α} {t : Set α} :
                          (s - t).Nonempty s.Nonempty t.Nonempty
                          @[simp]
                          theorem Set.div_nonempty {α : Type u_2} [Div α] {s : Set α} {t : Set α} :
                          (s / t).Nonempty s.Nonempty t.Nonempty
                          theorem Set.Nonempty.sub {α : Type u_2} [Sub α] {s : Set α} {t : Set α} :
                          s.Nonemptyt.Nonempty(s - t).Nonempty
                          theorem Set.Nonempty.div {α : Type u_2} [Div α] {s : Set α} {t : Set α} :
                          s.Nonemptyt.Nonempty(s / t).Nonempty
                          theorem Set.Nonempty.of_sub_left {α : Type u_2} [Sub α] {s : Set α} {t : Set α} :
                          (s - t).Nonemptys.Nonempty
                          theorem Set.Nonempty.of_div_left {α : Type u_2} [Div α] {s : Set α} {t : Set α} :
                          (s / t).Nonemptys.Nonempty
                          theorem Set.Nonempty.of_sub_right {α : Type u_2} [Sub α] {s : Set α} {t : Set α} :
                          (s - t).Nonemptyt.Nonempty
                          theorem Set.Nonempty.of_div_right {α : Type u_2} [Div α] {s : Set α} {t : Set α} :
                          (s / t).Nonemptyt.Nonempty
                          @[simp]
                          theorem Set.sub_singleton {α : Type u_2} [Sub α] {s : Set α} {b : α} :
                          s - {b} = (fun (x : α) => x - b) '' s
                          @[simp]
                          theorem Set.div_singleton {α : Type u_2} [Div α] {s : Set α} {b : α} :
                          s / {b} = (fun (x : α) => x / b) '' s
                          @[simp]
                          theorem Set.singleton_sub {α : Type u_2} [Sub α] {t : Set α} {a : α} :
                          {a} - t = (fun (x1 x2 : α) => x1 - x2) a '' t
                          @[simp]
                          theorem Set.singleton_div {α : Type u_2} [Div α] {t : Set α} {a : α} :
                          {a} / t = (fun (x1 x2 : α) => x1 / x2) a '' t
                          theorem Set.singleton_sub_singleton {α : Type u_2} [Sub α] {a : α} {b : α} :
                          {a} - {b} = {a - b}
                          theorem Set.singleton_div_singleton {α : Type u_2} [Div α] {a : α} {b : α} :
                          {a} / {b} = {a / b}
                          theorem Set.sub_subset_sub {α : Type u_2} [Sub α] {s₁ : Set α} {s₂ : Set α} {t₁ : Set α} {t₂ : Set α} :
                          s₁ t₁s₂ t₂s₁ - s₂ t₁ - t₂
                          theorem Set.div_subset_div {α : Type u_2} [Div α] {s₁ : Set α} {s₂ : Set α} {t₁ : Set α} {t₂ : Set α} :
                          s₁ t₁s₂ t₂s₁ / s₂ t₁ / t₂
                          theorem Set.sub_subset_sub_left {α : Type u_2} [Sub α] {s : Set α} {t₁ : Set α} {t₂ : Set α} :
                          t₁ t₂s - t₁ s - t₂
                          theorem Set.div_subset_div_left {α : Type u_2} [Div α] {s : Set α} {t₁ : Set α} {t₂ : Set α} :
                          t₁ t₂s / t₁ s / t₂
                          theorem Set.sub_subset_sub_right {α : Type u_2} [Sub α] {s₁ : Set α} {s₂ : Set α} {t : Set α} :
                          s₁ s₂s₁ - t s₂ - t
                          theorem Set.div_subset_div_right {α : Type u_2} [Div α] {s₁ : Set α} {s₂ : Set α} {t : Set α} :
                          s₁ s₂s₁ / t s₂ / t
                          theorem Set.sub_subset_iff {α : Type u_2} [Sub α] {s : Set α} {t : Set α} {u : Set α} :
                          s - t u xs, yt, x - y u
                          theorem Set.div_subset_iff {α : Type u_2} [Div α] {s : Set α} {t : Set α} {u : Set α} :
                          s / t u xs, yt, x / y u
                          theorem Set.union_sub {α : Type u_2} [Sub α] {s₁ : Set α} {s₂ : Set α} {t : Set α} :
                          s₁ s₂ - t = s₁ - t (s₂ - t)
                          theorem Set.union_div {α : Type u_2} [Div α] {s₁ : Set α} {s₂ : Set α} {t : Set α} :
                          (s₁ s₂) / t = s₁ / t s₂ / t
                          theorem Set.sub_union {α : Type u_2} [Sub α] {s : Set α} {t₁ : Set α} {t₂ : Set α} :
                          s - (t₁ t₂) = s - t₁ (s - t₂)
                          theorem Set.div_union {α : Type u_2} [Div α] {s : Set α} {t₁ : Set α} {t₂ : Set α} :
                          s / (t₁ t₂) = s / t₁ s / t₂
                          theorem Set.inter_sub_subset {α : Type u_2} [Sub α] {s₁ : Set α} {s₂ : Set α} {t : Set α} :
                          s₁ s₂ - t (s₁ - t) (s₂ - t)
                          theorem Set.inter_div_subset {α : Type u_2} [Div α] {s₁ : Set α} {s₂ : Set α} {t : Set α} :
                          s₁ s₂ / t s₁ / t (s₂ / t)
                          theorem Set.sub_inter_subset {α : Type u_2} [Sub α] {s : Set α} {t₁ : Set α} {t₂ : Set α} :
                          s - t₁ t₂ (s - t₁) (s - t₂)
                          theorem Set.div_inter_subset {α : Type u_2} [Div α] {s : Set α} {t₁ : Set α} {t₂ : Set α} :
                          s / (t₁ t₂) s / t₁ (s / t₂)
                          theorem Set.inter_sub_union_subset_union {α : Type u_2} [Sub α] {s₁ : Set α} {s₂ : Set α} {t₁ : Set α} {t₂ : Set α} :
                          s₁ s₂ - (t₁ t₂) s₁ - t₁ (s₂ - t₂)
                          theorem Set.inter_div_union_subset_union {α : Type u_2} [Div α] {s₁ : Set α} {s₂ : Set α} {t₁ : Set α} {t₂ : Set α} :
                          s₁ s₂ / (t₁ t₂) s₁ / t₁ s₂ / t₂
                          theorem Set.union_sub_inter_subset_union {α : Type u_2} [Sub α] {s₁ : Set α} {s₂ : Set α} {t₁ : Set α} {t₂ : Set α} :
                          s₁ s₂ - t₁ t₂ s₁ - t₁ (s₂ - t₂)
                          theorem Set.union_div_inter_subset_union {α : Type u_2} [Div α] {s₁ : Set α} {s₂ : Set α} {t₁ : Set α} {t₂ : Set α} :
                          (s₁ s₂) / (t₁ t₂) s₁ / t₁ s₂ / t₂
                          theorem Set.iUnion_sub_left_image {α : Type u_2} [Sub α] {s : Set α} {t : Set α} :
                          as, (fun (x : α) => a - x) '' t = s - t
                          theorem Set.iUnion_div_left_image {α : Type u_2} [Div α] {s : Set α} {t : Set α} :
                          as, (fun (x : α) => a / x) '' t = s / t
                          theorem Set.iUnion_sub_right_image {α : Type u_2} [Sub α] {s : Set α} {t : Set α} :
                          at, (fun (x : α) => x - a) '' s = s - t
                          theorem Set.iUnion_div_right_image {α : Type u_2} [Div α] {s : Set α} {t : Set α} :
                          at, (fun (x : α) => x / a) '' s = s / t
                          theorem Set.iUnion_sub {α : Type u_2} {ι : Sort u_5} [Sub α] (s : ιSet α) (t : Set α) :
                          (⋃ (i : ι), s i) - t = ⋃ (i : ι), s i - t
                          theorem Set.iUnion_div {α : Type u_2} {ι : Sort u_5} [Div α] (s : ιSet α) (t : Set α) :
                          (⋃ (i : ι), s i) / t = ⋃ (i : ι), s i / t
                          theorem Set.sub_iUnion {α : Type u_2} {ι : Sort u_5} [Sub α] (s : Set α) (t : ιSet α) :
                          s - ⋃ (i : ι), t i = ⋃ (i : ι), s - t i
                          theorem Set.div_iUnion {α : Type u_2} {ι : Sort u_5} [Div α] (s : Set α) (t : ιSet α) :
                          s / ⋃ (i : ι), t i = ⋃ (i : ι), s / t i
                          theorem Set.sUnion_sub {α : Type u_2} [Sub α] (S : Set (Set α)) (t : Set α) :
                          ⋃₀ S - t = sS, s - t
                          theorem Set.sUnion_div {α : Type u_2} [Div α] (S : Set (Set α)) (t : Set α) :
                          ⋃₀ S / t = sS, s / t
                          theorem Set.sub_sUnion {α : Type u_2} [Sub α] (s : Set α) (T : Set (Set α)) :
                          s - ⋃₀ T = tT, s - t
                          theorem Set.div_sUnion {α : Type u_2} [Div α] (s : Set α) (T : Set (Set α)) :
                          s / ⋃₀ T = tT, s / t
                          theorem Set.iUnion₂_sub {α : Type u_2} {ι : Sort u_5} {κ : ιSort u_6} [Sub α] (s : (i : ι) → κ iSet α) (t : Set α) :
                          (⋃ (i : ι), ⋃ (j : κ i), s i j) - t = ⋃ (i : ι), ⋃ (j : κ i), s i j - t
                          theorem Set.iUnion₂_div {α : Type u_2} {ι : Sort u_5} {κ : ιSort u_6} [Div α] (s : (i : ι) → κ iSet α) (t : Set α) :
                          (⋃ (i : ι), ⋃ (j : κ i), s i j) / t = ⋃ (i : ι), ⋃ (j : κ i), s i j / t
                          theorem Set.sub_iUnion₂ {α : Type u_2} {ι : Sort u_5} {κ : ιSort u_6} [Sub α] (s : Set α) (t : (i : ι) → κ iSet α) :
                          s - ⋃ (i : ι), ⋃ (j : κ i), t i j = ⋃ (i : ι), ⋃ (j : κ i), s - t i j
                          theorem Set.div_iUnion₂ {α : Type u_2} {ι : Sort u_5} {κ : ιSort u_6} [Div α] (s : Set α) (t : (i : ι) → κ iSet α) :
                          s / ⋃ (i : ι), ⋃ (j : κ i), t i j = ⋃ (i : ι), ⋃ (j : κ i), s / t i j
                          theorem Set.iInter_sub_subset {α : Type u_2} {ι : Sort u_5} [Sub α] (s : ιSet α) (t : Set α) :
                          (⋂ (i : ι), s i) - t ⋂ (i : ι), s i - t
                          theorem Set.iInter_div_subset {α : Type u_2} {ι : Sort u_5} [Div α] (s : ιSet α) (t : Set α) :
                          (⋂ (i : ι), s i) / t ⋂ (i : ι), s i / t
                          theorem Set.sub_iInter_subset {α : Type u_2} {ι : Sort u_5} [Sub α] (s : Set α) (t : ιSet α) :
                          s - ⋂ (i : ι), t i ⋂ (i : ι), s - t i
                          theorem Set.div_iInter_subset {α : Type u_2} {ι : Sort u_5} [Div α] (s : Set α) (t : ιSet α) :
                          s / ⋂ (i : ι), t i ⋂ (i : ι), s / t i
                          theorem Set.sInter_sub_subset {α : Type u_2} [Sub α] (S : Set (Set α)) (t : Set α) :
                          ⋂₀ S - t sS, s - t
                          theorem Set.sInter_div_subset {α : Type u_2} [Div α] (S : Set (Set α)) (t : Set α) :
                          ⋂₀ S / t sS, s / t
                          theorem Set.sub_sInter_subset {α : Type u_2} [Sub α] (s : Set α) (T : Set (Set α)) :
                          s - ⋂₀ T tT, s - t
                          theorem Set.div_sInter_subset {α : Type u_2} [Div α] (s : Set α) (T : Set (Set α)) :
                          s / ⋂₀ T tT, s / t
                          theorem Set.iInter₂_sub_subset {α : Type u_2} {ι : Sort u_5} {κ : ιSort u_6} [Sub α] (s : (i : ι) → κ iSet α) (t : Set α) :
                          (⋂ (i : ι), ⋂ (j : κ i), s i j) - t ⋂ (i : ι), ⋂ (j : κ i), s i j - t
                          theorem Set.iInter₂_div_subset {α : Type u_2} {ι : Sort u_5} {κ : ιSort u_6} [Div α] (s : (i : ι) → κ iSet α) (t : Set α) :
                          (⋂ (i : ι), ⋂ (j : κ i), s i j) / t ⋂ (i : ι), ⋂ (j : κ i), s i j / t
                          theorem Set.sub_iInter₂_subset {α : Type u_2} {ι : Sort u_5} {κ : ιSort u_6} [Sub α] (s : Set α) (t : (i : ι) → κ iSet α) :
                          s - ⋂ (i : ι), ⋂ (j : κ i), t i j ⋂ (i : ι), ⋂ (j : κ i), s - t i j
                          theorem Set.div_iInter₂_subset {α : Type u_2} {ι : Sort u_5} {κ : ιSort u_6} [Div α] (s : Set α) (t : (i : ι) → κ iSet α) :
                          s / ⋂ (i : ι), ⋂ (j : κ i), t i j ⋂ (i : ι), ⋂ (j : κ i), s / t i j

                          Translation/scaling of sets #

                          def Set.vaddSet {α : Type u_2} {β : Type u_3} [VAdd α β] :
                          VAdd α (Set β)

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

                          Equations
                          • Set.vaddSet = { vadd := fun (a : α) => Set.image fun (x : β) => a +ᵥ x }
                          Instances For
                            def Set.smulSet {α : Type u_2} {β : Type u_3} [SMul α β] :
                            SMul α (Set β)

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

                            Equations
                            • Set.smulSet = { smul := fun (a : α) => Set.image fun (x : β) => a x }
                            Instances For
                              def Set.vadd {α : Type u_2} {β : Type u_3} [VAdd α β] :
                              VAdd (Set α) (Set β)

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

                              Equations
                              Instances For
                                def Set.smul {α : Type u_2} {β : Type u_3} [SMul α β] :
                                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.smul = { smul := Set.image2 fun (x1 : α) (x2 : β) => x1 x2 }
                                Instances For
                                  @[simp]
                                  theorem Set.image2_vadd {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set α} {t : Set β} :
                                  Set.image2 VAdd.vadd s t = s +ᵥ t
                                  @[simp]
                                  theorem Set.image2_smul {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set α} {t : Set β} :
                                  Set.image2 SMul.smul s t = s t
                                  theorem Set.vadd_image_prod {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set α} {t : Set β} :
                                  (fun (x : α × β) => x.1 +ᵥ x.2) '' s ×ˢ t = s +ᵥ t
                                  theorem Set.image_smul_prod {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set α} {t : Set β} :
                                  (fun (x : α × β) => x.1 x.2) '' s ×ˢ t = s t
                                  theorem Set.mem_vadd {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set α} {t : Set β} {b : β} :
                                  b s +ᵥ t xs, yt, x +ᵥ y = b
                                  theorem Set.mem_smul {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set α} {t : Set β} {b : β} :
                                  b s t xs, yt, x y = b
                                  theorem Set.vadd_mem_vadd {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set α} {t : Set β} {a : α} {b : β} :
                                  a sb ta +ᵥ b s +ᵥ t
                                  theorem Set.smul_mem_smul {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set α} {t : Set β} {a : α} {b : β} :
                                  a sb ta b s t
                                  @[simp]
                                  theorem Set.empty_vadd {α : Type u_2} {β : Type u_3} [VAdd α β] {t : Set β} :
                                  @[simp]
                                  theorem Set.empty_smul {α : Type u_2} {β : Type u_3} [SMul α β] {t : Set β} :
                                  @[simp]
                                  theorem Set.vadd_empty {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set α} :
                                  @[simp]
                                  theorem Set.smul_empty {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set α} :
                                  @[simp]
                                  theorem Set.vadd_eq_empty {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set α} {t : Set β} :
                                  s +ᵥ t = s = t =
                                  @[simp]
                                  theorem Set.smul_eq_empty {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set α} {t : Set β} :
                                  s t = s = t =
                                  @[simp]
                                  theorem Set.vadd_nonempty {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set α} {t : Set β} :
                                  (s +ᵥ t).Nonempty s.Nonempty t.Nonempty
                                  @[simp]
                                  theorem Set.smul_nonempty {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set α} {t : Set β} :
                                  (s t).Nonempty s.Nonempty t.Nonempty
                                  theorem Set.Nonempty.vadd {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set α} {t : Set β} :
                                  s.Nonemptyt.Nonempty(s +ᵥ t).Nonempty
                                  theorem Set.Nonempty.smul {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set α} {t : Set β} :
                                  s.Nonemptyt.Nonempty(s t).Nonempty
                                  theorem Set.Nonempty.of_vadd_left {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set α} {t : Set β} :
                                  (s +ᵥ t).Nonemptys.Nonempty
                                  theorem Set.Nonempty.of_smul_left {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set α} {t : Set β} :
                                  (s t).Nonemptys.Nonempty
                                  theorem Set.Nonempty.of_vadd_right {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set α} {t : Set β} :
                                  (s +ᵥ t).Nonemptyt.Nonempty
                                  theorem Set.Nonempty.of_smul_right {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set α} {t : Set β} :
                                  (s t).Nonemptyt.Nonempty
                                  @[simp]
                                  theorem Set.vadd_singleton {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set α} {b : β} :
                                  s +ᵥ {b} = (fun (x : α) => x +ᵥ b) '' s
                                  @[simp]
                                  theorem Set.smul_singleton {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set α} {b : β} :
                                  s {b} = (fun (x : α) => x b) '' s
                                  @[simp]
                                  theorem Set.singleton_vadd {α : Type u_2} {β : Type u_3} [VAdd α β] {t : Set β} {a : α} :
                                  {a} +ᵥ t = a +ᵥ t
                                  @[simp]
                                  theorem Set.singleton_smul {α : Type u_2} {β : Type u_3} [SMul α β] {t : Set β} {a : α} :
                                  {a} t = a t
                                  @[simp]
                                  theorem Set.singleton_vadd_singleton {α : Type u_2} {β : Type u_3} [VAdd α β] {a : α} {b : β} :
                                  {a} +ᵥ {b} = {a +ᵥ b}
                                  @[simp]
                                  theorem Set.singleton_smul_singleton {α : Type u_2} {β : Type u_3} [SMul α β] {a : α} {b : β} :
                                  {a} {b} = {a b}
                                  theorem Set.vadd_subset_vadd {α : Type u_2} {β : Type u_3} [VAdd α β] {s₁ : Set α} {s₂ : Set α} {t₁ : Set β} {t₂ : Set β} :
                                  s₁ s₂t₁ t₂s₁ +ᵥ t₁ s₂ +ᵥ t₂
                                  theorem Set.smul_subset_smul {α : Type u_2} {β : Type u_3} [SMul α β] {s₁ : Set α} {s₂ : Set α} {t₁ : Set β} {t₂ : Set β} :
                                  s₁ s₂t₁ t₂s₁ t₁ s₂ t₂
                                  theorem Set.vadd_subset_vadd_left {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set α} {t₁ : Set β} {t₂ : Set β} :
                                  t₁ t₂s +ᵥ t₁ s +ᵥ t₂
                                  theorem Set.smul_subset_smul_left {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set α} {t₁ : Set β} {t₂ : Set β} :
                                  t₁ t₂s t₁ s t₂
                                  theorem Set.vadd_subset_vadd_right {α : Type u_2} {β : Type u_3} [VAdd α β] {s₁ : Set α} {s₂ : Set α} {t : Set β} :
                                  s₁ s₂s₁ +ᵥ t s₂ +ᵥ t
                                  theorem Set.smul_subset_smul_right {α : Type u_2} {β : Type u_3} [SMul α β] {s₁ : Set α} {s₂ : Set α} {t : Set β} :
                                  s₁ s₂s₁ t s₂ t
                                  theorem Set.vadd_subset_iff {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set α} {t : Set β} {u : Set β} :
                                  s +ᵥ t u as, bt, a +ᵥ b u
                                  theorem Set.smul_subset_iff {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set α} {t : Set β} {u : Set β} :
                                  s t u as, bt, a b u
                                  theorem Set.union_vadd {α : Type u_2} {β : Type u_3} [VAdd α β] {s₁ : Set α} {s₂ : Set α} {t : Set β} :
                                  s₁ s₂ +ᵥ t = s₁ +ᵥ t (s₂ +ᵥ t)
                                  theorem Set.union_smul {α : Type u_2} {β : Type u_3} [SMul α β] {s₁ : Set α} {s₂ : Set α} {t : Set β} :
                                  (s₁ s₂) t = s₁ t s₂ t
                                  theorem Set.vadd_union {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set α} {t₁ : Set β} {t₂ : Set β} :
                                  s +ᵥ (t₁ t₂) = s +ᵥ t₁ (s +ᵥ t₂)
                                  theorem Set.smul_union {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set α} {t₁ : Set β} {t₂ : Set β} :
                                  s (t₁ t₂) = s t₁ s t₂
                                  theorem Set.inter_vadd_subset {α : Type u_2} {β : Type u_3} [VAdd α β] {s₁ : Set α} {s₂ : Set α} {t : Set β} :
                                  s₁ s₂ +ᵥ t (s₁ +ᵥ t) (s₂ +ᵥ t)
                                  theorem Set.inter_smul_subset {α : Type u_2} {β : Type u_3} [SMul α β] {s₁ : Set α} {s₂ : Set α} {t : Set β} :
                                  (s₁ s₂) t s₁ t s₂ t
                                  theorem Set.vadd_inter_subset {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set α} {t₁ : Set β} {t₂ : Set β} :
                                  s +ᵥ t₁ t₂ (s +ᵥ t₁) (s +ᵥ t₂)
                                  theorem Set.smul_inter_subset {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set α} {t₁ : Set β} {t₂ : Set β} :
                                  s (t₁ t₂) s t₁ s t₂
                                  theorem Set.inter_vadd_union_subset_union {α : Type u_2} {β : Type u_3} [VAdd α β] {s₁ : Set α} {s₂ : Set α} {t₁ : Set β} {t₂ : Set β} :
                                  s₁ s₂ +ᵥ (t₁ t₂) s₁ +ᵥ t₁ (s₂ +ᵥ t₂)
                                  theorem Set.inter_smul_union_subset_union {α : Type u_2} {β : Type u_3} [SMul α β] {s₁ : Set α} {s₂ : Set α} {t₁ : Set β} {t₂ : Set β} :
                                  (s₁ s₂) (t₁ t₂) s₁ t₁ s₂ t₂
                                  theorem Set.union_vadd_inter_subset_union {α : Type u_2} {β : Type u_3} [VAdd α β] {s₁ : Set α} {s₂ : Set α} {t₁ : Set β} {t₂ : Set β} :
                                  s₁ s₂ +ᵥ t₁ t₂ s₁ +ᵥ t₁ (s₂ +ᵥ t₂)
                                  theorem Set.union_smul_inter_subset_union {α : Type u_2} {β : Type u_3} [SMul α β] {s₁ : Set α} {s₂ : Set α} {t₁ : Set β} {t₂ : Set β} :
                                  (s₁ s₂) (t₁ t₂) s₁ t₁ s₂ t₂
                                  theorem Set.iUnion_vadd_left_image {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set α} {t : Set β} :
                                  as, a +ᵥ t = s +ᵥ t
                                  theorem Set.iUnion_smul_left_image {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set α} {t : Set β} :
                                  as, a t = s t
                                  theorem Set.iUnion_vadd_right_image {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set α} {t : Set β} :
                                  at, (fun (x : α) => x +ᵥ a) '' s = s +ᵥ t
                                  theorem Set.iUnion_smul_right_image {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set α} {t : Set β} :
                                  at, (fun (x : α) => x a) '' s = s t
                                  theorem Set.iUnion_vadd {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [VAdd α β] (s : ιSet α) (t : Set β) :
                                  (⋃ (i : ι), s i) +ᵥ t = ⋃ (i : ι), s i +ᵥ t
                                  theorem Set.iUnion_smul {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [SMul α β] (s : ιSet α) (t : Set β) :
                                  (⋃ (i : ι), s i) t = ⋃ (i : ι), s i t
                                  theorem Set.vadd_iUnion {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [VAdd α β] (s : Set α) (t : ιSet β) :
                                  s +ᵥ ⋃ (i : ι), t i = ⋃ (i : ι), s +ᵥ t i
                                  theorem Set.smul_iUnion {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [SMul α β] (s : Set α) (t : ιSet β) :
                                  s ⋃ (i : ι), t i = ⋃ (i : ι), s t i
                                  theorem Set.sUnion_vadd {α : Type u_2} {β : Type u_3} [VAdd α β] (S : Set (Set α)) (t : Set β) :
                                  ⋃₀ S +ᵥ t = sS, s +ᵥ t
                                  theorem Set.sUnion_smul {α : Type u_2} {β : Type u_3} [SMul α β] (S : Set (Set α)) (t : Set β) :
                                  ⋃₀ S t = sS, s t
                                  theorem Set.vadd_sUnion {α : Type u_2} {β : Type u_3} [VAdd α β] (s : Set α) (T : Set (Set β)) :
                                  s +ᵥ ⋃₀ T = tT, s +ᵥ t
                                  theorem Set.smul_sUnion {α : Type u_2} {β : Type u_3} [SMul α β] (s : Set α) (T : Set (Set β)) :
                                  s ⋃₀ T = tT, s t
                                  theorem Set.iUnion₂_vadd {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ιSort u_6} [VAdd α β] (s : (i : ι) → κ iSet α) (t : Set β) :
                                  (⋃ (i : ι), ⋃ (j : κ i), s i j) +ᵥ t = ⋃ (i : ι), ⋃ (j : κ i), s i j +ᵥ t
                                  theorem Set.iUnion₂_smul {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ιSort u_6} [SMul α β] (s : (i : ι) → κ iSet α) (t : Set β) :
                                  (⋃ (i : ι), ⋃ (j : κ i), s i j) t = ⋃ (i : ι), ⋃ (j : κ i), s i j t
                                  theorem Set.vadd_iUnion₂ {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ιSort u_6} [VAdd α β] (s : Set α) (t : (i : ι) → κ iSet β) :
                                  s +ᵥ ⋃ (i : ι), ⋃ (j : κ i), t i j = ⋃ (i : ι), ⋃ (j : κ i), s +ᵥ t i j
                                  theorem Set.smul_iUnion₂ {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ιSort u_6} [SMul α β] (s : Set α) (t : (i : ι) → κ iSet β) :
                                  s ⋃ (i : ι), ⋃ (j : κ i), t i j = ⋃ (i : ι), ⋃ (j : κ i), s t i j
                                  theorem Set.iInter_vadd_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [VAdd α β] (s : ιSet α) (t : Set β) :
                                  (⋂ (i : ι), s i) +ᵥ t ⋂ (i : ι), s i +ᵥ t
                                  theorem Set.iInter_smul_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [SMul α β] (s : ιSet α) (t : Set β) :
                                  (⋂ (i : ι), s i) t ⋂ (i : ι), s i t
                                  theorem Set.vadd_iInter_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [VAdd α β] (s : Set α) (t : ιSet β) :
                                  s +ᵥ ⋂ (i : ι), t i ⋂ (i : ι), s +ᵥ t i
                                  theorem Set.smul_iInter_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [SMul α β] (s : Set α) (t : ιSet β) :
                                  s ⋂ (i : ι), t i ⋂ (i : ι), s t i
                                  theorem Set.sInter_vadd_subset {α : Type u_2} {β : Type u_3} [VAdd α β] (S : Set (Set α)) (t : Set β) :
                                  ⋂₀ S +ᵥ t sS, s +ᵥ t
                                  theorem Set.sInter_smul_subset {α : Type u_2} {β : Type u_3} [SMul α β] (S : Set (Set α)) (t : Set β) :
                                  ⋂₀ S t sS, s t
                                  theorem Set.vadd_sInter_subset {α : Type u_2} {β : Type u_3} [VAdd α β] (s : Set α) (T : Set (Set β)) :
                                  s +ᵥ ⋂₀ T tT, s +ᵥ t
                                  theorem Set.smul_sInter_subset {α : Type u_2} {β : Type u_3} [SMul α β] (s : Set α) (T : Set (Set β)) :
                                  s ⋂₀ T tT, s t
                                  theorem Set.iInter₂_vadd_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ιSort u_6} [VAdd α β] (s : (i : ι) → κ iSet α) (t : Set β) :
                                  (⋂ (i : ι), ⋂ (j : κ i), s i j) +ᵥ t ⋂ (i : ι), ⋂ (j : κ i), s i j +ᵥ t
                                  theorem Set.iInter₂_smul_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ιSort u_6} [SMul α β] (s : (i : ι) → κ iSet α) (t : Set β) :
                                  (⋂ (i : ι), ⋂ (j : κ i), s i j) t ⋂ (i : ι), ⋂ (j : κ i), s i j t
                                  theorem Set.vadd_iInter₂_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ιSort u_6} [VAdd α β] (s : Set α) (t : (i : ι) → κ iSet β) :
                                  s +ᵥ ⋂ (i : ι), ⋂ (j : κ i), t i j ⋂ (i : ι), ⋂ (j : κ i), s +ᵥ t i j
                                  theorem Set.smul_iInter₂_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ιSort u_6} [SMul α β] (s : Set α) (t : (i : ι) → κ iSet β) :
                                  s ⋂ (i : ι), ⋂ (j : κ i), t i j ⋂ (i : ι), ⋂ (j : κ i), s t i j
                                  theorem Set.vadd_set_subset_vadd {α : Type u_2} {β : Type u_3} [VAdd α β] {t : Set β} {a : α} {s : Set α} :
                                  a sa +ᵥ t s +ᵥ t
                                  theorem Set.smul_set_subset_smul {α : Type u_2} {β : Type u_3} [SMul α β] {t : Set β} {a : α} {s : Set α} :
                                  a sa t s t
                                  @[simp]
                                  theorem Set.iUnion_vadd_set {α : Type u_2} {β : Type u_3} [VAdd α β] (s : Set α) (t : Set β) :
                                  as, a +ᵥ t = s +ᵥ t
                                  @[simp]
                                  theorem Set.iUnion_smul_set {α : Type u_2} {β : Type u_3} [SMul α β] (s : Set α) (t : Set β) :
                                  as, a t = s t
                                  theorem Set.image_vadd {α : Type u_2} {β : Type u_3} [VAdd α β] {t : Set β} {a : α} :
                                  (fun (x : β) => a +ᵥ x) '' t = a +ᵥ t
                                  theorem Set.image_smul {α : Type u_2} {β : Type u_3} [SMul α β] {t : Set β} {a : α} :
                                  (fun (x : β) => a x) '' t = a t
                                  theorem Set.mem_vadd_set {α : Type u_2} {β : Type u_3} [VAdd α β] {t : Set β} {a : α} {x : β} :
                                  x a +ᵥ t yt, a +ᵥ y = x
                                  theorem Set.mem_smul_set {α : Type u_2} {β : Type u_3} [SMul α β] {t : Set β} {a : α} {x : β} :
                                  x a t yt, a y = x
                                  theorem Set.vadd_mem_vadd_set {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set β} {a : α} {b : β} :
                                  b sa +ᵥ b a +ᵥ s
                                  theorem Set.smul_mem_smul_set {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set β} {a : α} {b : β} :
                                  b sa b a s
                                  @[simp]
                                  theorem Set.vadd_set_empty {α : Type u_2} {β : Type u_3} [VAdd α β] {a : α} :
                                  @[simp]
                                  theorem Set.smul_set_empty {α : Type u_2} {β : Type u_3} [SMul α β] {a : α} :
                                  @[simp]
                                  theorem Set.vadd_set_eq_empty {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set β} {a : α} :
                                  a +ᵥ s = s =
                                  @[simp]
                                  theorem Set.smul_set_eq_empty {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set β} {a : α} :
                                  a s = s =
                                  @[simp]
                                  theorem Set.vadd_set_nonempty {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set β} {a : α} :
                                  (a +ᵥ s).Nonempty s.Nonempty
                                  @[simp]
                                  theorem Set.smul_set_nonempty {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set β} {a : α} :
                                  (a s).Nonempty s.Nonempty
                                  @[simp]
                                  theorem Set.vadd_set_singleton {α : Type u_2} {β : Type u_3} [VAdd α β] {a : α} {b : β} :
                                  a +ᵥ {b} = {a +ᵥ b}
                                  @[simp]
                                  theorem Set.smul_set_singleton {α : Type u_2} {β : Type u_3} [SMul α β] {a : α} {b : β} :
                                  a {b} = {a b}
                                  theorem Set.vadd_set_mono {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set β} {t : Set β} {a : α} :
                                  s ta +ᵥ s a +ᵥ t
                                  theorem Set.smul_set_mono {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set β} {t : Set β} {a : α} :
                                  s ta s a t
                                  theorem Set.vadd_set_subset_iff {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set β} {t : Set β} {a : α} :
                                  a +ᵥ s t ∀ ⦃b : β⦄, b sa +ᵥ b t
                                  theorem Set.smul_set_subset_iff {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set β} {t : Set β} {a : α} :
                                  a s t ∀ ⦃b : β⦄, b sa b t
                                  theorem Set.vadd_set_union {α : Type u_2} {β : Type u_3} [VAdd α β] {t₁ : Set β} {t₂ : Set β} {a : α} :
                                  a +ᵥ (t₁ t₂) = a +ᵥ t₁ (a +ᵥ t₂)
                                  theorem Set.smul_set_union {α : Type u_2} {β : Type u_3} [SMul α β] {t₁ : Set β} {t₂ : Set β} {a : α} :
                                  a (t₁ t₂) = a t₁ a t₂
                                  theorem Set.vadd_set_insert {α : Type u_2} {β : Type u_3} [VAdd α β] (a : α) (b : β) (s : Set β) :
                                  a +ᵥ insert b s = insert (a +ᵥ b) (a +ᵥ s)
                                  theorem Set.smul_set_insert {α : Type u_2} {β : Type u_3} [SMul α β] (a : α) (b : β) (s : Set β) :
                                  a insert b s = insert (a b) (a s)
                                  theorem Set.vadd_set_inter_subset {α : Type u_2} {β : Type u_3} [VAdd α β] {t₁ : Set β} {t₂ : Set β} {a : α} :
                                  a +ᵥ t₁ t₂ (a +ᵥ t₁) (a +ᵥ t₂)
                                  theorem Set.smul_set_inter_subset {α : Type u_2} {β : Type u_3} [SMul α β] {t₁ : Set β} {t₂ : Set β} {a : α} :
                                  a (t₁ t₂) a t₁ a t₂
                                  theorem Set.vadd_set_iUnion {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [VAdd α β] (a : α) (s : ιSet β) :
                                  a +ᵥ ⋃ (i : ι), s i = ⋃ (i : ι), a +ᵥ s i
                                  theorem Set.smul_set_iUnion {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [SMul α β] (a : α) (s : ιSet β) :
                                  a ⋃ (i : ι), s i = ⋃ (i : ι), a s i
                                  theorem Set.vadd_set_iUnion₂ {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ιSort u_6} [VAdd α β] (a : α) (s : (i : ι) → κ iSet β) :
                                  a +ᵥ ⋃ (i : ι), ⋃ (j : κ i), s i j = ⋃ (i : ι), ⋃ (j : κ i), a +ᵥ s i j
                                  theorem Set.smul_set_iUnion₂ {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ιSort u_6} [SMul α β] (a : α) (s : (i : ι) → κ iSet β) :
                                  a ⋃ (i : ι), ⋃ (j : κ i), s i j = ⋃ (i : ι), ⋃ (j : κ i), a s i j
                                  theorem Set.vadd_set_sUnion {α : Type u_2} {β : Type u_3} [VAdd α β] (a : α) (S : Set (Set β)) :
                                  a +ᵥ ⋃₀ S = sS, a +ᵥ s
                                  theorem Set.smul_set_sUnion {α : Type u_2} {β : Type u_3} [SMul α β] (a : α) (S : Set (Set β)) :
                                  a ⋃₀ S = sS, a s
                                  theorem Set.vadd_set_iInter_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [VAdd α β] (a : α) (t : ιSet β) :
                                  a +ᵥ ⋂ (i : ι), t i ⋂ (i : ι), a +ᵥ t i
                                  theorem Set.smul_set_iInter_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [SMul α β] (a : α) (t : ιSet β) :
                                  a ⋂ (i : ι), t i ⋂ (i : ι), a t i
                                  theorem Set.vadd_set_sInter_subset {α : Type u_2} {β : Type u_3} [VAdd α β] (a : α) (S : Set (Set β)) :
                                  a +ᵥ ⋂₀ S sS, a +ᵥ s
                                  theorem Set.smul_set_sInter_subset {α : Type u_2} {β : Type u_3} [SMul α β] (a : α) (S : Set (Set β)) :
                                  a ⋂₀ S sS, a s
                                  theorem Set.vadd_set_iInter₂_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ιSort u_6} [VAdd α β] (a : α) (t : (i : ι) → κ iSet β) :
                                  a +ᵥ ⋂ (i : ι), ⋂ (j : κ i), t i j ⋂ (i : ι), ⋂ (j : κ i), a +ᵥ t i j
                                  theorem Set.smul_set_iInter₂_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ιSort u_6} [SMul α β] (a : α) (t : (i : ι) → κ iSet β) :
                                  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} [VAdd α β] {s : Set β} {a : α} :
                                  s.Nonempty(a +ᵥ s).Nonempty
                                  theorem Set.Nonempty.smul_set {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set β} {a : α} :
                                  s.Nonempty(a s).Nonempty
                                  theorem Set.range_vadd_range {α : Type u_2} {β : Type u_3} {ι : Type u_5} {κ : Type u_6} [VAdd α β] (b : ια) (c : κβ) :
                                  Set.range b +ᵥ Set.range c = Set.range fun (p : ι × κ) => b p.1 +ᵥ c p.2
                                  theorem Set.range_smul_range {α : Type u_2} {β : Type u_3} {ι : Type u_5} {κ : Type u_6} [SMul α β] (b : ια) (c : κβ) :
                                  Set.range b Set.range c = Set.range fun (p : ι × κ) => b p.1 c p.2
                                  theorem Set.vadd_set_range {α : Type u_2} {β : Type u_3} [VAdd α β] {ι : Sort u_5} (a : α) (f : ιβ) :
                                  a +ᵥ Set.range f = Set.range fun (i : ι) => a +ᵥ f i
                                  theorem Set.smul_set_range {α : Type u_2} {β : Type u_3} [SMul α β] {ι : Sort u_5} (a : α) (f : ιβ) :
                                  a Set.range f = Set.range fun (i : ι) => a f i
                                  theorem Set.range_vadd {α : Type u_2} {β : Type u_3} [VAdd α β] {ι : Sort u_5} (a : α) (f : ιβ) :
                                  (Set.range fun (i : ι) => a +ᵥ f i) = a +ᵥ Set.range f
                                  theorem Set.range_smul {α : Type u_2} {β : Type u_3} [SMul α β] {ι : Sort u_5} (a : α) (f : ιβ) :
                                  (Set.range fun (i : ι) => a f i) = a Set.range f
                                  instance Set.vsub {α : Type u_2} {β : Type u_3} [VSub α β] :
                                  VSub (Set α) (Set β)
                                  Equations
                                  @[simp]
                                  theorem Set.image2_vsub {α : Type u_2} {β : Type u_3} [VSub α β] {s : Set β} {t : Set β} :
                                  Set.image2 VSub.vsub s t = s -ᵥ t
                                  theorem Set.image_vsub_prod {α : Type u_2} {β : Type u_3} [VSub α β] {s : Set β} {t : Set β} :
                                  (fun (x : β × β) => x.1 -ᵥ x.2) '' s ×ˢ t = s -ᵥ t
                                  theorem Set.mem_vsub {α : Type u_2} {β : Type u_3} [VSub α β] {s : Set β} {t : Set β} {a : α} :
                                  a s -ᵥ t xs, yt, x -ᵥ y = a
                                  theorem Set.vsub_mem_vsub {α : Type u_2} {β : Type u_3} [VSub α β] {s : Set β} {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} [VSub α β] (t : Set β) :
                                  @[simp]
                                  theorem Set.vsub_empty {α : Type u_2} {β : Type u_3} [VSub α β] (s : Set β) :
                                  @[simp]
                                  theorem Set.vsub_eq_empty {α : Type u_2} {β : Type u_3} [VSub α β] {s : Set β} {t : Set β} :
                                  s -ᵥ t = s = t =
                                  @[simp]
                                  theorem Set.vsub_nonempty {α : Type u_2} {β : Type u_3} [VSub α β] {s : Set β} {t : Set β} :
                                  (s -ᵥ t).Nonempty s.Nonempty t.Nonempty
                                  theorem Set.Nonempty.vsub {α : Type u_2} {β : Type u_3} [VSub α β] {s : Set β} {t : Set β} :
                                  s.Nonemptyt.Nonempty(s -ᵥ t).Nonempty
                                  theorem Set.Nonempty.of_vsub_left {α : Type u_2} {β : Type u_3} [VSub α β] {s : Set β} {t : Set β} :
                                  (s -ᵥ t).Nonemptys.Nonempty
                                  theorem Set.Nonempty.of_vsub_right {α : Type u_2} {β : Type u_3} [VSub α β] {s : Set β} {t : Set β} :
                                  (s -ᵥ t).Nonemptyt.Nonempty
                                  @[simp]
                                  theorem Set.vsub_singleton {α : Type u_2} {β : Type u_3} [VSub α β] (s : Set β) (b : β) :
                                  s -ᵥ {b} = (fun (x : β) => x -ᵥ b) '' s
                                  @[simp]
                                  theorem Set.singleton_vsub {α : Type u_2} {β : Type u_3} [VSub α β] (t : Set β) (b : β) :
                                  {b} -ᵥ t = (fun (x : β) => b -ᵥ x) '' t
                                  @[simp]
                                  theorem Set.singleton_vsub_singleton {α : Type u_2} {β : Type u_3} [VSub α β] {b : β} {c : β} :
                                  {b} -ᵥ {c} = {b -ᵥ c}
                                  theorem Set.vsub_subset_vsub {α : Type u_2} {β : Type u_3} [VSub α β] {s₁ : Set β} {s₂ : Set β} {t₁ : Set β} {t₂ : Set β} :
                                  s₁ s₂t₁ t₂s₁ -ᵥ t₁ s₂ -ᵥ t₂
                                  theorem Set.vsub_subset_vsub_left {α : Type u_2} {β : Type u_3} [VSub α β] {s : Set β} {t₁ : Set β} {t₂ : Set β} :
                                  t₁ t₂s -ᵥ t₁ s -ᵥ t₂
                                  theorem Set.vsub_subset_vsub_right {α : Type u_2} {β : Type u_3} [VSub α β] {s₁ : Set β} {s₂ : Set β} {t : Set β} :
                                  s₁ s₂s₁ -ᵥ t s₂ -ᵥ t
                                  theorem Set.vsub_subset_iff {α : Type u_2} {β : Type u_3} [VSub α β] {s : Set β} {t : Set β} {u : Set α} :
                                  s -ᵥ t u xs, yt, x -ᵥ y u
                                  theorem Set.vsub_self_mono {α : Type u_2} {β : Type u_3} [VSub α β] {s : Set β} {t : Set β} (h : s t) :
                                  s -ᵥ s t -ᵥ t
                                  theorem Set.union_vsub {α : Type u_2} {β : Type u_3} [VSub α β] {s₁ : Set β} {s₂ : Set β} {t : Set β} :
                                  s₁ s₂ -ᵥ t = s₁ -ᵥ t (s₂ -ᵥ t)
                                  theorem Set.vsub_union {α : Type u_2} {β : Type u_3} [VSub α β] {s : Set β} {t₁ : Set β} {t₂ : Set β} :
                                  s -ᵥ (t₁ t₂) = s -ᵥ t₁ (s -ᵥ t₂)
                                  theorem Set.inter_vsub_subset {α : Type u_2} {β : Type u_3} [VSub α β] {s₁ : Set β} {s₂ : Set β} {t : Set β} :
                                  s₁ s₂ -ᵥ t (s₁ -ᵥ t) (s₂ -ᵥ t)
                                  theorem Set.vsub_inter_subset {α : Type u_2} {β : Type u_3} [VSub α β] {s : Set β} {t₁ : Set β} {t₂ : Set β} :
                                  s -ᵥ t₁ t₂ (s -ᵥ t₁) (s -ᵥ t₂)
                                  theorem Set.inter_vsub_union_subset_union {α : Type u_2} {β : Type u_3} [VSub α β] {s₁ : Set β} {s₂ : Set β} {t₁ : Set β} {t₂ : Set β} :
                                  s₁ s₂ -ᵥ (t₁ t₂) s₁ -ᵥ t₁ (s₂ -ᵥ t₂)
                                  theorem Set.union_vsub_inter_subset_union {α : Type u_2} {β : Type u_3} [VSub α β] {s₁ : Set β} {s₂ : Set β} {t₁ : Set β} {t₂ : Set β} :
                                  s₁ s₂ -ᵥ t₁ t₂ s₁ -ᵥ t₁ (s₂ -ᵥ t₂)
                                  theorem Set.iUnion_vsub_left_image {α : Type u_2} {β : Type u_3} [VSub α β] {s : Set β} {t : Set β} :
                                  as, (fun (x : β) => a -ᵥ x) '' t = s -ᵥ t
                                  theorem Set.iUnion_vsub_right_image {α : Type u_2} {β : Type u_3} [VSub α β] {s : Set β} {t : Set β} :
                                  at, (fun (x : β) => x -ᵥ a) '' s = s -ᵥ t
                                  theorem Set.iUnion_vsub {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [VSub α β] (s : ιSet β) (t : Set β) :
                                  (⋃ (i : ι), s i) -ᵥ t = ⋃ (i : ι), s i -ᵥ t
                                  theorem Set.vsub_iUnion {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [VSub α β] (s : Set β) (t : ιSet β) :
                                  s -ᵥ ⋃ (i : ι), t i = ⋃ (i : ι), s -ᵥ t i
                                  theorem Set.sUnion_vsub {α : Type u_2} {β : Type u_3} [VSub α β] (S : Set (Set β)) (t : Set β) :
                                  ⋃₀ S -ᵥ t = sS, s -ᵥ t
                                  theorem Set.vsub_sUnion {α : Type u_2} {β : Type u_3} [VSub α β] (s : Set β) (T : Set (Set β)) :
                                  s -ᵥ ⋃₀ T = tT, s -ᵥ t
                                  theorem Set.iUnion₂_vsub {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ιSort u_6} [VSub α β] (s : (i : ι) → κ iSet β) (t : Set β) :
                                  (⋃ (i : ι), ⋃ (j : κ i), s i j) -ᵥ t = ⋃ (i : ι), ⋃ (j : κ i), s i j -ᵥ t
                                  theorem Set.vsub_iUnion₂ {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ιSort u_6} [VSub α β] (s : Set β) (t : (i : ι) → κ iSet β) :
                                  s -ᵥ ⋃ (i : ι), ⋃ (j : κ i), t i j = ⋃ (i : ι), ⋃ (j : κ i), s -ᵥ t i j
                                  theorem Set.iInter_vsub_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [VSub α β] (s : ιSet β) (t : Set β) :
                                  (⋂ (i : ι), s i) -ᵥ t ⋂ (i : ι), s i -ᵥ t
                                  theorem Set.vsub_iInter_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [VSub α β] (s : Set β) (t : ιSet β) :
                                  s -ᵥ ⋂ (i : ι), t i ⋂ (i : ι), s -ᵥ t i
                                  theorem Set.sInter_vsub_subset {α : Type u_2} {β : Type u_3} [VSub α β] (S : Set (Set β)) (t : Set β) :
                                  ⋂₀ S -ᵥ t sS, s -ᵥ t
                                  theorem Set.vsub_sInter_subset {α : Type u_2} {β : Type u_3} [VSub α β] (s : Set β) (T : Set (Set β)) :
                                  s -ᵥ ⋂₀ T tT, s -ᵥ t
                                  theorem Set.iInter₂_vsub_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ιSort u_6} [VSub α β] (s : (i : ι) → κ iSet β) (t : Set β) :
                                  (⋂ (i : ι), ⋂ (j : κ i), s i j) -ᵥ t ⋂ (i : ι), ⋂ (j : κ i), s i j -ᵥ t
                                  theorem Set.vsub_iInter₂_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ιSort u_6} [VSub α β] (s : Set β) (t : (i : ι) → κ iSet β) :
                                  s -ᵥ ⋂ (i : ι), ⋂ (j : κ i), t i j ⋂ (i : ι), ⋂ (j : κ i), s -ᵥ t i j
                                  theorem Set.image_vadd_comm {α : Type u_2} {β : Type u_3} {γ : Type u_4} [VAdd α β] [VAdd α γ] (f : βγ) (a : α) (s : Set β) :
                                  (∀ (b : β), f (a +ᵥ b) = a +ᵥ f b)f '' (a +ᵥ s) = a +ᵥ f '' s
                                  theorem Set.image_smul_comm {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SMul α β] [SMul α γ] (f : βγ) (a : α) (s : Set β) :
                                  (∀ (b : β), f (a b) = a f b)f '' (a s) = a f '' s
                                  def Set.NSMul {α : Type u_2} [Zero α] [Add α] :
                                  SMul (Set α)

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

                                  Equations
                                  • Set.NSMul = { smul := nsmulRec }
                                  Instances For
                                    def Set.NPow {α : Type u_2} [One α] [Mul α] :
                                    Pow (Set α)

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

                                    Equations
                                    Instances For
                                      def Set.ZSMul {α : Type u_2} [Zero α] [Add α] [Neg α] :
                                      SMul (Set α)

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

                                      Equations
                                      • Set.ZSMul = { smul := zsmulRec }
                                      Instances For
                                        def Set.ZPow {α : Type u_2} [One α] [Mul α] [Inv α] :
                                        Pow (Set α)

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

                                        Equations
                                        • Set.ZPow = { pow := fun (s : Set α) (n : ) => zpowRec npowRec n s }
                                        Instances For
                                          noncomputable def Set.addSemigroup {α : Type u_2} [AddSemigroup α] :

                                          Set α is an AddSemigroup under pointwise operations if α is.

                                          Equations
                                          Instances For
                                            noncomputable def Set.semigroup {α : Type u_2} [Semigroup α] :

                                            Set α is a Semigroup under pointwise operations if α is.

                                            Equations
                                            Instances For
                                              noncomputable def Set.addCommSemigroup {α : Type u_2} [AddCommSemigroup α] :

                                              Set α is an AddCommSemigroup under pointwise operations if α is.

                                              Equations
                                              Instances For
                                                noncomputable def Set.commSemigroup {α : Type u_2} [CommSemigroup α] :

                                                Set α is a CommSemigroup under pointwise operations if α is.

                                                Equations
                                                Instances For
                                                  theorem Set.inter_add_union_subset {α : Type u_2} [AddCommSemigroup α] {s : Set α} {t : Set α} :
                                                  s t + (s t) s + t
                                                  theorem Set.inter_mul_union_subset {α : Type u_2} [CommSemigroup α] {s : Set α} {t : Set α} :
                                                  s t * (s t) s * t
                                                  theorem Set.union_add_inter_subset {α : Type u_2} [AddCommSemigroup α] {s : Set α} {t : Set α} :
                                                  s t + s t s + t
                                                  theorem Set.union_mul_inter_subset {α : Type u_2} [CommSemigroup α] {s : Set α} {t : Set α} :
                                                  (s t) * (s t) s * t
                                                  noncomputable def Set.addZeroClass {α : Type u_2} [AddZeroClass α] :

                                                  Set α is an AddZeroClass under pointwise operations if α is.

                                                  Equations
                                                  Instances For
                                                    noncomputable def Set.mulOneClass {α : Type u_2} [MulOneClass α] :

                                                    Set α is a MulOneClass under pointwise operations if α is.

                                                    Equations
                                                    Instances For
                                                      theorem Set.subset_add_left {α : Type u_2} [AddZeroClass α] (s : Set α) {t : Set α} (ht : 0 t) :
                                                      s s + t
                                                      theorem Set.subset_mul_left {α : Type u_2} [MulOneClass α] (s : Set α) {t : Set α} (ht : 1 t) :
                                                      s s * t
                                                      theorem Set.subset_add_right {α : Type u_2} [AddZeroClass α] {s : Set α} (t : Set α) (hs : 0 s) :
                                                      t s + t
                                                      theorem Set.subset_mul_right {α : Type u_2} [MulOneClass α] {s : Set α} (t : Set α) (hs : 1 s) :
                                                      t s * t
                                                      noncomputable def Set.singletonAddMonoidHom {α : Type u_2} [AddZeroClass α] :
                                                      α →+ Set α

                                                      The singleton operation as an AddMonoidHom.

                                                      Equations
                                                      • Set.singletonAddMonoidHom = { toFun := Set.singletonAddHom.toFun, map_zero' := , map_add' := }
                                                      Instances For
                                                        noncomputable def Set.singletonMonoidHom {α : Type u_2} [MulOneClass α] :
                                                        α →* Set α

                                                        The singleton operation as a MonoidHom.

                                                        Equations
                                                        • Set.singletonMonoidHom = { toFun := Set.singletonMulHom.toFun, map_one' := , map_mul' := }
                                                        Instances For
                                                          @[simp]
                                                          theorem Set.coe_singletonAddMonoidHom {α : Type u_2} [AddZeroClass α] :
                                                          Set.singletonAddMonoidHom = singleton
                                                          @[simp]
                                                          theorem Set.coe_singletonMonoidHom {α : Type u_2} [MulOneClass α] :
                                                          Set.singletonMonoidHom = singleton
                                                          @[simp]
                                                          theorem Set.singletonAddMonoidHom_apply {α : Type u_2} [AddZeroClass α] (a : α) :
                                                          Set.singletonAddMonoidHom a = {a}
                                                          @[simp]
                                                          theorem Set.singletonMonoidHom_apply {α : Type u_2} [MulOneClass α] (a : α) :
                                                          Set.singletonMonoidHom a = {a}
                                                          noncomputable def Set.addMonoid {α : Type u_2} [AddMonoid α] :

                                                          Set α is an AddMonoid under pointwise operations if α is.

                                                          Equations
                                                          Instances For
                                                            noncomputable def Set.monoid {α : Type u_2} [Monoid α] :
                                                            Monoid (Set α)

                                                            Set α is a Monoid under pointwise operations if α is.

                                                            Equations
                                                            • Set.monoid = Monoid.mk npowRecAuto
                                                            Instances For
                                                              theorem Set.nsmul_mem_nsmul {α : Type u_2} [AddMonoid α] {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} [AddMonoid α] {s : Set α} {t : Set α} (hst : s t) (n : ) :
                                                              n s n t
                                                              theorem Set.pow_subset_pow {α : Type u_2} [Monoid α] {s : Set α} {t : Set α} (hst : s t) (n : ) :
                                                              s ^ n t ^ n
                                                              theorem Set.nsmul_subset_nsmul_of_zero_mem {α : Type u_2} [AddMonoid α] {s : Set α} {m : } {n : } (hs : 0 s) (hn : m n) :
                                                              m s n s
                                                              theorem Set.pow_subset_pow_of_one_mem {α : Type u_2} [Monoid α] {s : Set α} {m : } {n : } (hs : 1 s) (hn : m n) :
                                                              s ^ m s ^ n
                                                              @[simp]
                                                              theorem Set.nsmul_empty {α : Type u_2} [AddMonoid α] {n : } (hn : n 0) :
                                                              @[simp]
                                                              theorem Set.empty_pow {α : Type u_2} [Monoid α] {n : } (hn : n 0) :
                                                              @[deprecated Set.nsmul_empty]
                                                              theorem Set.empty_nsmul {α : Type u_2} [AddMonoid α] {n : } (hn : n 0) :

                                                              Alias of Set.nsmul_empty.

                                                              @[simp]
                                                              theorem Set.nsmul_singleton {α : Type u_2} [AddMonoid α] (a : α) (n : ) :
                                                              n {a} = {n a}
                                                              @[simp]
                                                              theorem Set.singleton_pow {α : Type u_2} [Monoid α] (a : α) (n : ) :
                                                              {a} ^ n = {a ^ n}
                                                              theorem Set.add_univ_of_zero_mem {α : Type u_2} [AddMonoid α] {s : Set α} (hs : 0 s) :
                                                              s + Set.univ = Set.univ
                                                              theorem Set.mul_univ_of_one_mem {α : Type u_2} [Monoid α] {s : Set α} (hs : 1 s) :
                                                              s * Set.univ = Set.univ
                                                              theorem Set.univ_add_of_zero_mem {α : Type u_2} [AddMonoid α] {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} [AddMonoid α] :
                                                              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_2} [AddMonoid α] {n : } :
                                                              n 0n Set.univ = Set.univ
                                                              @[simp]
                                                              theorem Set.univ_pow {α : Type u_2} [Monoid α] {n : } :
                                                              n 0Set.univ ^ n = Set.univ
                                                              theorem IsAddUnit.set {α : Type u_2} [AddMonoid α] {a : α} :
                                                              theorem IsUnit.set {α : Type u_2} [Monoid α] {a : α} :
                                                              IsUnit aIsUnit {a}
                                                              noncomputable def Set.addCommMonoid {α : Type u_2} [AddCommMonoid α] :

                                                              Set α is an AddCommMonoid under pointwise operations if α is.

                                                              Equations
                                                              Instances For
                                                                noncomputable def Set.commMonoid {α : Type u_2} [CommMonoid α] :

                                                                Set α is a CommMonoid under pointwise operations if α is.

                                                                Equations
                                                                Instances For
                                                                  theorem Set.add_eq_zero_iff {α : Type u_2} [SubtractionMonoid α] {s : Set α} {t : Set α} :
                                                                  s + t = 0 ∃ (a : α) (b : α), s = {a} t = {b} a + b = 0
                                                                  theorem Set.mul_eq_one_iff {α : Type u_2} [DivisionMonoid α] {s : Set α} {t : Set α} :
                                                                  s * t = 1 ∃ (a : α) (b : α), s = {a} t = {b} a * b = 1
                                                                  noncomputable def Set.subtractionMonoid {α : Type u_2} [SubtractionMonoid α] :

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

                                                                  Equations
                                                                  Instances For
                                                                    noncomputable def Set.divisionMonoid {α : Type u_2} [DivisionMonoid α] :

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

                                                                    Equations
                                                                    Instances For
                                                                      @[simp]
                                                                      theorem Set.isAddUnit_iff {α : Type u_2} [SubtractionMonoid α] {s : Set α} :
                                                                      IsAddUnit s ∃ (a : α), s = {a} IsAddUnit a
                                                                      @[simp]
                                                                      theorem Set.isUnit_iff {α : Type u_2} [DivisionMonoid α] {s : Set α} :
                                                                      IsUnit s ∃ (a : α), s = {a} IsUnit a
                                                                      @[simp]
                                                                      theorem Set.univ_sub_univ {α : Type u_2} [SubtractionMonoid α] :
                                                                      Set.univ - Set.univ = Set.univ
                                                                      @[simp]
                                                                      theorem Set.univ_div_univ {α : Type u_2} [DivisionMonoid α] :
                                                                      Set.univ / Set.univ = Set.univ
                                                                      theorem Set.subset_sub_left {α : Type u_2} [SubtractionMonoid α] {s : Set α} {t : Set α} (ht : 0 t) :
                                                                      s s - t
                                                                      theorem Set.subset_div_left {α : Type u_2} [DivisionMonoid α] {s : Set α} {t : Set α} (ht : 1 t) :
                                                                      s s / t
                                                                      theorem Set.neg_subset_sub_right {α : Type u_2} [SubtractionMonoid α] {s : Set α} {t : Set α} (hs : 0 s) :
                                                                      -t s - t
                                                                      theorem Set.inv_subset_div_right {α : Type u_2} [DivisionMonoid α] {s : Set α} {t : Set α} (hs : 1 s) :
                                                                      t⁻¹ s / t
                                                                      @[simp]
                                                                      theorem Set.zsmul_empty {α : Type u_2} [SubtractionMonoid α] {n : } (hn : n 0) :
                                                                      @[simp]
                                                                      theorem Set.empty_zpow {α : Type u_2} [DivisionMonoid α] {n : } (hn : n 0) :
                                                                      @[simp]
                                                                      theorem Set.zsmul_singleton {α : Type u_2} [SubtractionMonoid α] (a : α) (n : ) :
                                                                      n {a} = {n a}
                                                                      @[simp]
                                                                      theorem Set.singleton_zpow {α : Type u_2} [DivisionMonoid α] (a : α) (n : ) :
                                                                      {a} ^ n = {a ^ n}

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

                                                                      Equations
                                                                      Instances For
                                                                        noncomputable def Set.divisionCommMonoid {α : Type u_2} [DivisionCommMonoid α] :

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

                                                                        Equations
                                                                        Instances For

                                                                          Note that Set is not a Group because s / s ≠ 1 in general.

                                                                          @[simp]
                                                                          theorem Set.zero_mem_sub_iff {α : Type u_2} [AddGroup α] {s : Set α} {t : Set α} :
                                                                          0 s - t ¬Disjoint s t
                                                                          @[simp]
                                                                          theorem Set.one_mem_div_iff {α : Type u_2} [Group α] {s : Set α} {t : Set α} :
                                                                          1 s / t ¬Disjoint s t
                                                                          theorem Set.not_zero_mem_sub_iff {α : Type u_2} [AddGroup α] {s : Set α} {t : Set α} :
                                                                          0s - t Disjoint s t
                                                                          theorem Set.not_one_mem_div_iff {α : Type u_2} [Group α] {s : Set α} {t : Set α} :
                                                                          1s / t Disjoint s t
                                                                          theorem Disjoint.one_not_mem_div_set {α : Type u_2} [Group α] {s : Set α} {t : Set α} :
                                                                          Disjoint s t1s / t

                                                                          Alias of the reverse direction of Set.not_one_mem_div_iff.

                                                                          theorem Disjoint.zero_not_mem_sub_set {α : Type u_2} [AddGroup α] {s : Set α} {t : Set α} :
                                                                          Disjoint s t0s - t
                                                                          theorem Set.Nonempty.zero_mem_sub {α : Type u_2} [AddGroup α] {s : Set α} (h : s.Nonempty) :
                                                                          0 s - s
                                                                          theorem Set.Nonempty.one_mem_div {α : Type u_2} [Group α] {s : Set α} (h : s.Nonempty) :
                                                                          1 s / s
                                                                          theorem Set.isAddUnit_singleton {α : Type u_2} [AddGroup α] (a : α) :
                                                                          theorem Set.isUnit_singleton {α : Type u_2} [Group α] (a : α) :
                                                                          IsUnit {a}
                                                                          @[simp]
                                                                          theorem Set.isAddUnit_iff_singleton {α : Type u_2} [AddGroup α] {s : Set α} :
                                                                          IsAddUnit s ∃ (a : α), s = {a}
                                                                          @[simp]
                                                                          theorem Set.isUnit_iff_singleton {α : Type u_2} [Group α] {s : Set α} :
                                                                          IsUnit s ∃ (a : α), s = {a}
                                                                          @[simp]
                                                                          theorem Set.image_add_left {α : Type u_2} [AddGroup α] {t : Set α} {a : α} :
                                                                          (fun (x : α) => a + x) '' t = (fun (x : α) => -a + x) ⁻¹' t
                                                                          @[simp]
                                                                          theorem Set.image_mul_left {α : Type u_2} [Group α] {t : Set α} {a : α} :
                                                                          (fun (x : α) => a * x) '' t = (fun (x : α) => a⁻¹ * x) ⁻¹' t
                                                                          @[simp]
                                                                          theorem Set.image_add_right {α : Type u_2} [AddGroup α] {t : Set α} {b : α} :
                                                                          (fun (x : α) => x + b) '' t = (fun (x : α) => x + -b) ⁻¹' t
                                                                          @[simp]
                                                                          theorem Set.image_mul_right {α : Type u_2} [Group α] {t : Set α} {b : α} :
                                                                          (fun (x : α) => x * b) '' t = (fun (x : α) => x * b⁻¹) ⁻¹' t
                                                                          theorem Set.image_add_left' {α : Type u_2} [AddGroup α] {t : Set α} {a : α} :
                                                                          (fun (x : α) => -a + x) '' t = (fun (x : α) => a + x) ⁻¹' t
                                                                          theorem Set.image_mul_left' {α : Type u_2} [Group α] {t : Set α} {a : α} :
                                                                          (fun (x : α) => a⁻¹ * x) '' t = (fun (x : α) => a * x) ⁻¹' t
                                                                          theorem Set.image_add_right' {α : Type u_2} [AddGroup α] {t : Set α} {b : α} :
                                                                          (fun (x : α) => x + -b) '' t = (fun (x : α) => x + b) ⁻¹' t
                                                                          theorem Set.image_mul_right' {α : Type u_2} [Group α] {t : Set α} {b : α} :
                                                                          (fun (x : α) => x * b⁻¹) '' t = (fun (x : α) => x * b) ⁻¹' t
                                                                          @[simp]
                                                                          theorem Set.preimage_add_left_singleton {α : Type u_2} [AddGroup α] {a : α} {b : α} :
                                                                          (fun (x : α) => a + x) ⁻¹' {b} = {-a + b}
                                                                          @[simp]
                                                                          theorem Set.preimage_mul_left_singleton {α : Type u_2} [Group α] {a : α} {b : α} :
                                                                          (fun (x : α) => a * x) ⁻¹' {b} = {a⁻¹ * b}
                                                                          @[simp]
                                                                          theorem Set.preimage_add_right_singleton {α : Type u_2} [AddGroup α] {a : α} {b : α} :
                                                                          (fun (x : α) => x + a) ⁻¹' {b} = {b + -a}
                                                                          @[simp]
                                                                          theorem Set.preimage_mul_right_singleton {α : Type u_2} [Group α] {a : α} {b : α} :
                                                                          (fun (x : α) => x * a) ⁻¹' {b} = {b * a⁻¹}
                                                                          @[simp]
                                                                          theorem Set.preimage_add_left_zero {α : Type u_2} [AddGroup α] {a : α} :
                                                                          (fun (x : α) => a + x) ⁻¹' 0 = {-a}
                                                                          @[simp]
                                                                          theorem Set.preimage_mul_left_one {α : Type u_2} [Group α] {a : α} :
                                                                          (fun (x : α) => a * x) ⁻¹' 1 = {a⁻¹}
                                                                          @[simp]
                                                                          theorem Set.preimage_add_right_zero {α : Type u_2} [AddGroup α] {b : α} :
                                                                          (fun (x : α) => x + b) ⁻¹' 0 = {-b}
                                                                          @[simp]
                                                                          theorem Set.preimage_mul_right_one {α : Type u_2} [Group α] {b : α} :
                                                                          (fun (x : α) => x * b) ⁻¹' 1 = {b⁻¹}
                                                                          theorem Set.preimage_add_left_zero' {α : Type u_2} [AddGroup α] {a : α} :
                                                                          (fun (x : α) => -a + x) ⁻¹' 0 = {a}
                                                                          theorem Set.preimage_mul_left_one' {α : Type u_2} [Group α] {a : α} :
                                                                          (fun (x : α) => a⁻¹ * x) ⁻¹' 1 = {a}
                                                                          theorem Set.preimage_add_right_zero' {α : Type u_2} [AddGroup α] {b : α} :
                                                                          (fun (x : α) => x + -b) ⁻¹' 0 = {b}
                                                                          theorem Set.preimage_mul_right_one' {α : Type u_2} [Group α] {b : α} :
                                                                          (fun (x : α) => x * b⁻¹) ⁻¹' 1 = {b}
                                                                          @[simp]
                                                                          theorem Set.add_univ {α : Type u_2} [AddGroup α] {s : Set α} (hs : s.Nonempty) :
                                                                          s + Set.univ = Set.univ
                                                                          @[simp]
                                                                          theorem Set.mul_univ {α : Type u_2} [Group α] {s : Set α} (hs : s.Nonempty) :
                                                                          s * Set.univ = Set.univ
                                                                          @[simp]
                                                                          theorem Set.univ_add {α : Type u_2} [AddGroup α] {t : Set α} (ht : t.Nonempty) :
                                                                          Set.univ + t = Set.univ
                                                                          @[simp]
                                                                          theorem Set.univ_mul {α : Type u_2} [Group α] {t : Set α} (ht : t.Nonempty) :
                                                                          Set.univ * t = Set.univ
                                                                          theorem Set.image_add {F : Type u_1} {α : Type u_2} {β : Type u_3} [Add α] [Add β] [FunLike F α β] [AddHomClass F α β] (m : F) {s : Set α} {t : Set α} :
                                                                          m '' (s + t) = m '' s + m '' t
                                                                          theorem Set.image_mul {F : Type u_1} {α : Type u_2} {β : Type u_3} [Mul α] [Mul β] [FunLike F α β] [MulHomClass F α β] (m : F) {s : Set α} {t : Set α} :
                                                                          m '' (s * t) = m '' s * m '' t
                                                                          theorem Set.add_subset_range {F : Type u_1} {α : Type u_2} {β : Type u_3} [Add α] [Add β] [FunLike F α β] [AddHomClass F α β] (m : F) {s : Set β} {t : Set β} (hs : s Set.range m) (ht : t Set.range m) :
                                                                          s + t Set.range m
                                                                          theorem Set.mul_subset_range {F : Type u_1} {α : Type u_2} {β : Type u_3} [Mul α] [Mul β] [FunLike F α β] [MulHomClass F α β] (m : F) {s : Set β} {t : Set β} (hs : s Set.range m) (ht : t Set.range m) :
                                                                          s * t Set.range m
                                                                          theorem Set.preimage_add_preimage_subset {F : Type u_1} {α : Type u_2} {β : Type u_3} [Add α] [Add β] [FunLike F α β] [AddHomClass F α β] (m : F) {s : Set β} {t : Set β} :
                                                                          m ⁻¹' s + m ⁻¹' t m ⁻¹' (s + t)
                                                                          theorem Set.preimage_mul_preimage_subset {F : Type u_1} {α : Type u_2} {β : Type u_3} [Mul α] [Mul β] [FunLike F α β] [MulHomClass F α β] (m : F) {s : Set β} {t : Set β} :
                                                                          m ⁻¹' s * m ⁻¹' t m ⁻¹' (s * t)
                                                                          theorem Set.preimage_add {F : Type u_1} {α : Type u_2} {β : Type u_3} [Add α] [Add β] [FunLike F α β] [AddHomClass F α β] (m : F) (hm : Function.Injective m) {s : Set β} {t : Set β} (hs : s Set.range m) (ht : t Set.range m) :
                                                                          m ⁻¹' (s + t) = m ⁻¹' s + m ⁻¹' t
                                                                          theorem Set.preimage_mul {F : Type u_1} {α : Type u_2} {β : Type u_3} [Mul α] [Mul β] [FunLike F α β] [MulHomClass F α β] (m : F) (hm : Function.Injective m) {s : Set β} {t : Set β} (hs : s Set.range m) (ht : t Set.range m) :
                                                                          m ⁻¹' (s * t) = m ⁻¹' s * m ⁻¹' t
                                                                          theorem Set.image_sub {F : Type u_1} {α : Type u_2} {β : Type u_3} [AddGroup α] [SubtractionMonoid β] [FunLike F α β] [AddMonoidHomClass F α β] (m : F) {s : Set α} {t : Set α} :
                                                                          m '' (s - t) = m '' s - m '' t
                                                                          theorem Set.image_div {F : Type u_1} {α : Type u_2} {β : Type u_3} [Group α] [DivisionMonoid β] [FunLike F α β] [MonoidHomClass F α β] (m : F) {s : Set α} {t : Set α} :
                                                                          m '' (s / t) = m '' s / m '' t
                                                                          theorem Set.sub_subset_range {F : Type u_1} {α : Type u_2} {β : Type u_3} [AddGroup α] [SubtractionMonoid β] [FunLike F α β] [AddMonoidHomClass F α β] (m : F) {s : Set β} {t : Set β} (hs : s Set.range m) (ht : t Set.range m) :
                                                                          s - t Set.range m
                                                                          theorem Set.div_subset_range {F : Type u_1} {α : Type u_2} {β : Type u_3} [Group α] [DivisionMonoid β] [FunLike F α β] [MonoidHomClass F α β] (m : F) {s : Set β} {t : Set β} (hs : s Set.range m) (ht : t Set.range m) :
                                                                          s / t Set.range m
                                                                          theorem Set.preimage_sub_preimage_subset {F : Type u_1} {α : Type u_2} {β : Type u_3} [AddGroup α] [SubtractionMonoid β] [FunLike F α β] [AddMonoidHomClass F α β] (m : F) {s : Set β} {t : Set β} :
                                                                          m ⁻¹' s - m ⁻¹' t m ⁻¹' (s - t)
                                                                          theorem Set.preimage_div_preimage_subset {F : Type u_1} {α : Type u_2} {β : Type u_3} [Group α] [DivisionMonoid β] [FunLike F α β] [MonoidHomClass F α β] (m : F) {s : Set β} {t : Set β} :
                                                                          m ⁻¹' s / m ⁻¹' t m ⁻¹' (s / t)
                                                                          theorem Set.preimage_sub {F : Type u_1} {α : Type u_2} {β : Type u_3} [AddGroup α] [SubtractionMonoid β] [FunLike F α β] [AddMonoidHomClass F α β] (m : F) (hm : Function.Injective m) {s : Set β} {t : Set β} (hs : s Set.range m) (ht : t Set.range m) :
                                                                          m ⁻¹' (s - t) = m ⁻¹' s - m ⁻¹' t
                                                                          theorem Set.preimage_div {F : Type u_1} {α : Type u_2} {β : Type u_3} [Group α] [DivisionMonoid β] [FunLike F α β] [MonoidHomClass F α β] (m : F) (hm : Function.Injective m) {s : Set β} {t : Set β} (hs : s Set.range m) (ht : t Set.range m) :
                                                                          m ⁻¹' (s / t) = m ⁻¹' s / m ⁻¹' t

                                                                          Miscellaneous #

                                                                          theorem AddGroup.card_nsmul_eq_card_nsmul_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 kf k = f B
                                                                          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 kf k = f B