Documentation

Mathlib.Data.Set.Pointwise.SMul

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.

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

Implementation notes #

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 (x : α) (x_1 : β) => x x_1 }
        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.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.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_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_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_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.op_vadd_set_subset_add {α : Type u_2} [Add α] {s : Set α} {t : Set α} {a : α} :
          a tAddOpposite.op a +ᵥ s s + t
          theorem Set.op_smul_set_subset_mul {α : Type u_2} [Mul α] {s : Set α} {t : Set α} {a : α} :
          a tMulOpposite.op a s s * t
          theorem Set.image_op_vadd {α : Type u_2} [Add α] {s : Set α} {t : Set α} :
          AddOpposite.op '' s +ᵥ t = t + s
          theorem Set.image_op_smul {α : Type u_2} [Mul α] {s : Set α} {t : Set α} :
          MulOpposite.op '' s t = t * s
          @[simp]
          theorem Set.iUnion_op_vadd_set {α : Type u_2} [Add α] (s : Set α) (t : Set α) :
          at, AddOpposite.op a +ᵥ s = s + t
          @[simp]
          theorem Set.iUnion_op_smul_set {α : Type u_2} [Mul α] (s : Set α) (t : Set α) :
          at, MulOpposite.op a s = s * t
          theorem Set.add_subset_iff_left {α : Type u_2} [Add α] {s : Set α} {t : Set α} {u : Set α} :
          s + t u as, a +ᵥ t u
          theorem Set.mul_subset_iff_left {α : Type u_2} [Mul α] {s : Set α} {t : Set α} {u : Set α} :
          s * t u as, a t u
          theorem Set.add_subset_iff_right {α : Type u_2} [Add α] {s : Set α} {t : Set α} {u : Set α} :
          s + t u bt, AddOpposite.op b +ᵥ s u
          theorem Set.mul_subset_iff_right {α : Type u_2} [Mul α] {s : Set α} {t : Set α} {u : Set α} :
          s * t u bt, MulOpposite.op b s u
          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} {a : α} [VAdd α β] {ι : Sort u_5} {f : ιβ} :
          a +ᵥ Set.range f = Set.range fun (i : ι) => a +ᵥ f i
          theorem Set.smul_set_range {α : Type u_2} {β : Type u_3} {a : α} [SMul α β] {ι : Sort u_5} {f : ιβ} :
          a Set.range f = Set.range fun (i : ι) => a f i
          instance Set.vaddCommClass_set {α : Type u_2} {β : Type u_3} {γ : Type u_4} [VAdd α γ] [VAdd β γ] [VAddCommClass α β γ] :
          VAddCommClass α β (Set γ)
          Equations
          • =
          instance Set.smulCommClass_set {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SMul α γ] [SMul β γ] [SMulCommClass α β γ] :
          SMulCommClass α β (Set γ)
          Equations
          • =
          instance Set.vaddCommClass_set' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [VAdd α γ] [VAdd β γ] [VAddCommClass α β γ] :
          VAddCommClass α (Set β) (Set γ)
          Equations
          • =
          instance Set.smulCommClass_set' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SMul α γ] [SMul β γ] [SMulCommClass α β γ] :
          SMulCommClass α (Set β) (Set γ)
          Equations
          • =
          instance Set.vaddCommClass_set'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [VAdd α γ] [VAdd β γ] [VAddCommClass α β γ] :
          VAddCommClass (Set α) β (Set γ)
          Equations
          • =
          instance Set.smulCommClass_set'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SMul α γ] [SMul β γ] [SMulCommClass α β γ] :
          SMulCommClass (Set α) β (Set γ)
          Equations
          • =
          instance Set.vaddCommClass {α : Type u_2} {β : Type u_3} {γ : Type u_4} [VAdd α γ] [VAdd β γ] [VAddCommClass α β γ] :
          VAddCommClass (Set α) (Set β) (Set γ)
          Equations
          • =
          instance Set.smulCommClass {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SMul α γ] [SMul β γ] [SMulCommClass α β γ] :
          SMulCommClass (Set α) (Set β) (Set γ)
          Equations
          • =
          instance Set.vaddAssocClass {α : Type u_2} {β : Type u_3} {γ : Type u_4} [VAdd α β] [VAdd α γ] [VAdd β γ] [VAddAssocClass α β γ] :
          VAddAssocClass α β (Set γ)
          Equations
          • =
          instance Set.isScalarTower {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SMul α β] [SMul α γ] [SMul β γ] [IsScalarTower α β γ] :
          IsScalarTower α β (Set γ)
          Equations
          • =
          instance Set.vaddAssocClass' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [VAdd α β] [VAdd α γ] [VAdd β γ] [VAddAssocClass α β γ] :
          VAddAssocClass α (Set β) (Set γ)
          Equations
          • =
          instance Set.isScalarTower' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SMul α β] [SMul α γ] [SMul β γ] [IsScalarTower α β γ] :
          IsScalarTower α (Set β) (Set γ)
          Equations
          • =
          instance Set.vaddAssocClass'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [VAdd α β] [VAdd α γ] [VAdd β γ] [VAddAssocClass α β γ] :
          VAddAssocClass (Set α) (Set β) (Set γ)
          Equations
          • =
          instance Set.isScalarTower'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SMul α β] [SMul α γ] [SMul β γ] [IsScalarTower α β γ] :
          IsScalarTower (Set α) (Set β) (Set γ)
          Equations
          • =
          instance Set.isCentralVAdd {α : Type u_2} {β : Type u_3} [VAdd α β] [VAdd αᵃᵒᵖ β] [IsCentralVAdd α β] :
          Equations
          • =
          instance Set.isCentralScalar {α : Type u_2} {β : Type u_3} [SMul α β] [SMul αᵐᵒᵖ β] [IsCentralScalar α β] :
          Equations
          • =
          theorem Set.addAction.proof_2 {α : Type u_1} {β : Type u_2} [AddMonoid α] [AddAction α β] :
          ∀ (x x_1 : Set α) (x_2 : Set β), Set.image2 (fun (x : α) (x_3 : β) => x +ᵥ x_3) (Set.image2 (fun (x x_3 : α) => x + x_3) x x_1) x_2 = Set.image2 (fun (x : α) (x_3 : β) => x +ᵥ x_3) x (Set.image2 (fun (x : α) (x_3 : β) => x +ᵥ x_3) x_1 x_2)
          def Set.addAction {α : Type u_2} {β : Type u_3} [AddMonoid α] [AddAction α β] :
          AddAction (Set α) (Set β)

          An additive action of an additive monoid α on a type β gives an additive action of Set α on Set β

          Equations
          Instances For
            theorem Set.addAction.proof_1 {α : Type u_2} {β : Type u_1} [AddMonoid α] [AddAction α β] (s : Set β) :
            Set.image2 (fun (x : α) (x_1 : β) => x +ᵥ x_1) {0} s = s
            def Set.mulAction {α : Type u_2} {β : Type u_3} [Monoid α] [MulAction α β] :
            MulAction (Set α) (Set β)

            A multiplicative action of a monoid α on a type β gives a multiplicative action of Set α on Set β.

            Equations
            Instances For
              theorem Set.addActionSet.proof_1 {α : Type u_2} {β : Type u_1} [AddMonoid α] [AddAction α β] :
              ∀ (x : Set β), (fun (x : β) => 0 +ᵥ x) '' x = x
              theorem Set.addActionSet.proof_2 {α : Type u_2} {β : Type u_1} [AddMonoid α] [AddAction α β] :
              ∀ (x x_1 : α) (x_2 : Set β), (fun (x_3 : β) => x + x_1 +ᵥ x_3) '' x_2 = (fun (x_3 : β) => x +ᵥ x_3) '' ((fun (x : β) => x_1 +ᵥ x) '' x_2)
              def Set.addActionSet {α : Type u_2} {β : Type u_3} [AddMonoid α] [AddAction α β] :
              AddAction α (Set β)

              An additive action of an additive monoid on a type β gives an additive action on Set β.

              Equations
              Instances For
                def Set.mulActionSet {α : Type u_2} {β : Type u_3} [Monoid α] [MulAction α β] :
                MulAction α (Set β)

                A multiplicative action of a monoid on a type β gives a multiplicative action on Set β.

                Equations
                Instances For
                  def Set.smulZeroClassSet {α : Type u_2} {β : Type u_3} [Zero β] [SMulZeroClass α β] :

                  If scalar multiplication by elements of α sends (0 : β) to zero, then the same is true for (0 : Set β).

                  Equations
                  Instances For
                    def Set.distribSMulSet {α : Type u_2} {β : Type u_3} [AddZeroClass β] [DistribSMul α β] :

                    If the scalar multiplication (· • ·) : α → β → β is distributive, then so is (· • ·) : α → Set β → Set β.

                    Equations
                    Instances For
                      def Set.distribMulActionSet {α : Type u_2} {β : Type u_3} [Monoid α] [AddMonoid β] [DistribMulAction α β] :

                      A distributive multiplicative action of a monoid on an additive monoid β gives a distributive multiplicative action on Set β.

                      Equations
                      Instances For
                        def Set.mulDistribMulActionSet {α : Type u_2} {β : Type u_3} [Monoid α] [Monoid β] [MulDistribMulAction α β] :

                        A multiplicative action of a monoid on a monoid β gives a multiplicative action on Set β.

                        Equations
                        Instances For
                          instance Set.instNoZeroSMulDivisors {α : Type u_2} {β : Type u_3} [Zero α] [Zero β] [SMul α β] [NoZeroSMulDivisors α β] :
                          Equations
                          • =
                          instance Set.noZeroSMulDivisors_set {α : Type u_2} {β : Type u_3} [Zero α] [Zero β] [SMul α β] [NoZeroSMulDivisors α β] :
                          Equations
                          • =
                          instance Set.instNoZeroDivisors {α : Type u_2} [Zero α] [Mul α] [NoZeroDivisors α] :
                          Equations
                          • =
                          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.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.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
                          theorem Set.image_vadd_distrib {F : Type u_1} {α : Type u_2} {β : Type u_3} [AddZeroClass α] [AddZeroClass β] [FunLike F α β] [AddMonoidHomClass F α β] (f : F) (a : α) (s : Set α) :
                          f '' (a +ᵥ s) = f a +ᵥ f '' s
                          theorem Set.image_smul_distrib {F : Type u_1} {α : Type u_2} {β : Type u_3} [MulOneClass α] [MulOneClass β] [FunLike F α β] [MonoidHomClass F α β] (f : F) (a : α) (s : Set α) :
                          f '' (a s) = f a f '' s
                          theorem Set.op_vadd_set_vadd_eq_vadd_vadd_set {α : Type u_2} {β : Type u_3} {γ : Type u_4} [VAdd αᵃᵒᵖ β] [VAdd β γ] [VAdd α γ] (a : α) (s : Set β) (t : Set γ) (h : ∀ (a : α) (b : β) (c : γ), AddOpposite.op a +ᵥ b +ᵥ c = b +ᵥ (a +ᵥ c)) :
                          theorem Set.op_smul_set_smul_eq_smul_smul_set {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SMul αᵐᵒᵖ β] [SMul β γ] [SMul α γ] (a : α) (s : Set β) (t : Set γ) (h : ∀ (a : α) (b : β) (c : γ), (MulOpposite.op a b) c = b a c) :
                          (MulOpposite.op a s) t = s a t
                          theorem Set.smul_zero_subset {α : Type u_2} {β : Type u_3} [Zero β] [SMulZeroClass α β] (s : Set α) :
                          s 0 0
                          theorem Set.Nonempty.smul_zero {α : Type u_2} {β : Type u_3} [Zero β] [SMulZeroClass α β] {s : Set α} (hs : s.Nonempty) :
                          s 0 = 0
                          theorem Set.zero_mem_smul_set {α : Type u_2} {β : Type u_3} [Zero β] [SMulZeroClass α β] {t : Set β} {a : α} (h : 0 t) :
                          0 a t
                          theorem Set.zero_mem_smul_set_iff {α : Type u_2} {β : Type u_3} [Zero β] [SMulZeroClass α β] {t : Set β} {a : α} [Zero α] [NoZeroSMulDivisors α β] (ha : a 0) :
                          0 a t 0 t

                          Note that we have neither SMulWithZero α (Set β) nor SMulWithZero (Set α) (Set β) because 0 * ∅ ≠ 0.

                          theorem Set.zero_smul_subset {α : Type u_2} {β : Type u_3} [Zero α] [Zero β] [SMulWithZero α β] (t : Set β) :
                          0 t 0
                          theorem Set.Nonempty.zero_smul {α : Type u_2} {β : Type u_3} [Zero α] [Zero β] [SMulWithZero α β] {t : Set β} (ht : t.Nonempty) :
                          0 t = 0
                          @[simp]
                          theorem Set.zero_smul_set {α : Type u_2} {β : Type u_3} [Zero α] [Zero β] [SMulWithZero α β] {s : Set β} (h : s.Nonempty) :
                          0 s = 0

                          A nonempty set is scaled by zero to the singleton set containing 0.

                          theorem Set.zero_smul_set_subset {α : Type u_2} {β : Type u_3} [Zero α] [Zero β] [SMulWithZero α β] (s : Set β) :
                          0 s 0
                          theorem Set.subsingleton_zero_smul_set {α : Type u_2} {β : Type u_3} [Zero α] [Zero β] [SMulWithZero α β] (s : Set β) :
                          (0 s).Subsingleton
                          theorem Set.zero_mem_smul_iff {α : Type u_2} {β : Type u_3} [Zero α] [Zero β] [SMulWithZero α β] {s : Set α} {t : Set β} [NoZeroSMulDivisors α β] :
                          0 s t 0 s t.Nonempty 0 t s.Nonempty
                          theorem Set.op_vadd_set_add_eq_add_vadd_set {α : Type u_2} [AddSemigroup α] (a : α) (s : Set α) (t : Set α) :
                          AddOpposite.op a +ᵥ s + t = s + (a +ᵥ t)
                          theorem Set.op_smul_set_mul_eq_mul_smul_set {α : Type u_2} [Semigroup α] (a : α) (s : Set α) (t : Set α) :
                          MulOpposite.op a s * t = s * a t
                          theorem Set.pairwiseDisjoint_vadd_iff {α : Type u_2} [Add α] [IsLeftCancelAdd α] {s : Set α} {t : Set α} :
                          (s.PairwiseDisjoint fun (x : α) => x +ᵥ t) Set.InjOn (fun (p : α × α) => p.1 + p.2) (s ×ˢ t)
                          theorem Set.pairwiseDisjoint_smul_iff {α : Type u_2} [Mul α] [IsLeftCancelMul α] {s : Set α} {t : Set α} :
                          (s.PairwiseDisjoint fun (x : α) => x t) Set.InjOn (fun (p : α × α) => p.1 * p.2) (s ×ˢ t)
                          @[simp]
                          theorem Set.vadd_mem_vadd_set_iff {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] {s : Set β} {a : α} {x : β} :
                          a +ᵥ x a +ᵥ s x s
                          @[simp]
                          theorem Set.smul_mem_smul_set_iff {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] {s : Set β} {a : α} {x : β} :
                          a x a s x s
                          theorem Set.mem_vadd_set_iff_neg_vadd_mem {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] {A : Set β} {a : α} {x : β} :
                          x a +ᵥ A -a +ᵥ x A
                          theorem Set.mem_smul_set_iff_inv_smul_mem {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] {A : Set β} {a : α} {x : β} :
                          x a A a⁻¹ x A
                          theorem Set.mem_neg_vadd_set_iff {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] {A : Set β} {a : α} {x : β} :
                          x -a +ᵥ A a +ᵥ x A
                          theorem Set.mem_inv_smul_set_iff {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] {A : Set β} {a : α} {x : β} :
                          x a⁻¹ A a x A
                          theorem Set.preimage_vadd {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] (a : α) (t : Set β) :
                          (fun (x : β) => a +ᵥ x) ⁻¹' t = -a +ᵥ t
                          theorem Set.preimage_smul {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] (a : α) (t : Set β) :
                          (fun (x : β) => a x) ⁻¹' t = a⁻¹ t
                          theorem Set.preimage_vadd_neg {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] (a : α) (t : Set β) :
                          (fun (x : β) => -a +ᵥ x) ⁻¹' t = a +ᵥ t
                          theorem Set.preimage_smul_inv {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] (a : α) (t : Set β) :
                          (fun (x : β) => a⁻¹ x) ⁻¹' t = a t
                          @[simp]
                          theorem Set.set_vadd_subset_set_vadd_iff {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] {A : Set β} {B : Set β} {a : α} :
                          a +ᵥ A a +ᵥ B A B
                          @[simp]
                          theorem Set.set_smul_subset_set_smul_iff {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] {A : Set β} {B : Set β} {a : α} :
                          a A a B A B
                          theorem Set.set_vadd_subset_iff {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] {A : Set β} {B : Set β} {a : α} :
                          a +ᵥ A B A -a +ᵥ B
                          theorem Set.set_smul_subset_iff {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] {A : Set β} {B : Set β} {a : α} :
                          a A B A a⁻¹ B
                          theorem Set.subset_set_vadd_iff {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] {A : Set β} {B : Set β} {a : α} :
                          A a +ᵥ B -a +ᵥ A B
                          theorem Set.subset_set_smul_iff {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] {A : Set β} {B : Set β} {a : α} :
                          A a B a⁻¹ A B
                          theorem Set.vadd_set_inter {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] {s : Set β} {t : Set β} {a : α} :
                          a +ᵥ s t = (a +ᵥ s) (a +ᵥ t)
                          theorem Set.smul_set_inter {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] {s : Set β} {t : Set β} {a : α} :
                          a (s t) = a s a t
                          theorem Set.vadd_set_iInter {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] {ι : Type u_5} (a : α) (t : ιSet β) :
                          a +ᵥ ⋂ (i : ι), t i = ⋂ (i : ι), a +ᵥ t i
                          theorem Set.smul_set_iInter {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] {ι : Type u_5} (a : α) (t : ιSet β) :
                          a ⋂ (i : ι), t i = ⋂ (i : ι), a t i
                          theorem Set.vadd_set_sdiff {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] {s : Set β} {t : Set β} {a : α} :
                          a +ᵥ s \ t = (a +ᵥ s) \ (a +ᵥ t)
                          theorem Set.smul_set_sdiff {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] {s : Set β} {t : Set β} {a : α} :
                          a (s \ t) = a s \ a t
                          theorem Set.vadd_set_symmDiff {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] {s : Set β} {t : Set β} {a : α} :
                          a +ᵥ symmDiff s t = symmDiff (a +ᵥ s) (a +ᵥ t)
                          theorem Set.smul_set_symmDiff {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] {s : Set β} {t : Set β} {a : α} :
                          a symmDiff s t = symmDiff (a s) (a t)
                          @[simp]
                          theorem Set.vadd_set_univ {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] {a : α} :
                          a +ᵥ Set.univ = Set.univ
                          @[simp]
                          theorem Set.smul_set_univ {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] {a : α} :
                          a Set.univ = Set.univ
                          @[simp]
                          theorem Set.vadd_univ {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] {s : Set α} (hs : s.Nonempty) :
                          s +ᵥ Set.univ = Set.univ
                          abbrev Set.vadd_univ.match_1 {α : Type u_1} {s : Set α} (motive : s.NonemptyProp) :
                          ∀ (hs : s.Nonempty), (∀ (a : α) (ha : a s), motive )motive hs
                          Equations
                          • =
                          Instances For
                            @[simp]
                            theorem Set.smul_univ {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] {s : Set α} (hs : s.Nonempty) :
                            s Set.univ = Set.univ
                            theorem Set.vadd_set_compl {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] {s : Set β} {a : α} :
                            a +ᵥ s = (a +ᵥ s)
                            theorem Set.smul_set_compl {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] {s : Set β} {a : α} :
                            a s = (a s)
                            theorem Set.vadd_inter_ne_empty_iff {α : Type u_2} [AddGroup α] {s : Set α} {t : Set α} {x : α} :
                            (x +ᵥ s) t ∃ (a : α) (b : α), (a t b s) a + -b = x
                            theorem Set.smul_inter_ne_empty_iff {α : Type u_2} [Group α] {s : Set α} {t : Set α} {x : α} :
                            x s t ∃ (a : α) (b : α), (a t b s) a * b⁻¹ = x
                            theorem Set.vadd_inter_ne_empty_iff' {α : Type u_2} [AddGroup α] {s : Set α} {t : Set α} {x : α} :
                            (x +ᵥ s) t ∃ (a : α) (b : α), (a t b s) a - b = x
                            theorem Set.smul_inter_ne_empty_iff' {α : Type u_2} [Group α] {s : Set α} {t : Set α} {x : α} :
                            x s t ∃ (a : α) (b : α), (a t b s) a / b = x
                            theorem Set.op_vadd_inter_ne_empty_iff {α : Type u_2} [AddGroup α] {s : Set α} {t : Set α} {x : αᵃᵒᵖ} :
                            (x +ᵥ s) t ∃ (a : α) (b : α), (a s b t) -a + b = AddOpposite.unop x
                            theorem Set.op_smul_inter_ne_empty_iff {α : Type u_2} [Group α] {s : Set α} {t : Set α} {x : αᵐᵒᵖ} :
                            x s t ∃ (a : α) (b : α), (a s b t) a⁻¹ * b = MulOpposite.unop x
                            @[simp]
                            theorem Set.iUnion_neg_vadd {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] {s : Set β} :
                            ⋃ (g : α), -g +ᵥ s = ⋃ (g : α), g +ᵥ s
                            @[simp]
                            theorem Set.iUnion_inv_smul {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] {s : Set β} :
                            ⋃ (g : α), g⁻¹ s = ⋃ (g : α), g s
                            theorem Set.iUnion_vadd_eq_setOf_exists {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] {s : Set β} :
                            ⋃ (g : α), g +ᵥ s = {a : β | ∃ (g : α), g +ᵥ a s}
                            theorem Set.iUnion_smul_eq_setOf_exists {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] {s : Set β} :
                            ⋃ (g : α), g s = {a : β | ∃ (g : α), g a s}
                            @[simp]
                            theorem Set.neg_vadd_set_distrib {α : Type u_2} [AddGroup α] (a : α) (s : Set α) :
                            @[simp]
                            theorem Set.inv_smul_set_distrib {α : Type u_2} [Group α] (a : α) (s : Set α) :
                            @[simp]
                            theorem Set.neg_op_vadd_set_distrib {α : Type u_2} [AddGroup α] (a : α) (s : Set α) :
                            @[simp]
                            theorem Set.inv_op_smul_set_distrib {α : Type u_2} [Group α] (a : α) (s : Set α) :
                            @[simp]
                            theorem Set.vadd_set_disjoint_iff {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] {s : Set β} {t : Set β} {a : α} :
                            Disjoint (a +ᵥ s) (a +ᵥ t) Disjoint s t
                            @[simp]
                            theorem Set.smul_set_disjoint_iff {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] {s : Set β} {t : Set β} {a : α} :
                            Disjoint (a s) (a t) Disjoint s t
                            @[simp]
                            theorem Set.smul_mem_smul_set_iff₀ {α : Type u_2} {β : Type u_3} [GroupWithZero α] [MulAction α β] {a : α} (ha : a 0) (A : Set β) (x : β) :
                            a x a A x A
                            theorem Set.mem_smul_set_iff_inv_smul_mem₀ {α : Type u_2} {β : Type u_3} [GroupWithZero α] [MulAction α β] {a : α} (ha : a 0) (A : Set β) (x : β) :
                            x a A a⁻¹ x A
                            theorem Set.mem_inv_smul_set_iff₀ {α : Type u_2} {β : Type u_3} [GroupWithZero α] [MulAction α β] {a : α} (ha : a 0) (A : Set β) (x : β) :
                            x a⁻¹ A a x A
                            theorem Set.preimage_smul₀ {α : Type u_2} {β : Type u_3} [GroupWithZero α] [MulAction α β] {a : α} (ha : a 0) (t : Set β) :
                            (fun (x : β) => a x) ⁻¹' t = a⁻¹ t
                            theorem Set.preimage_smul_inv₀ {α : Type u_2} {β : Type u_3} [GroupWithZero α] [MulAction α β] {a : α} (ha : a 0) (t : Set β) :
                            (fun (x : β) => a⁻¹ x) ⁻¹' t = a t
                            @[simp]
                            theorem Set.set_smul_subset_set_smul_iff₀ {α : Type u_2} {β : Type u_3} [GroupWithZero α] [MulAction α β] {a : α} (ha : a 0) {A : Set β} {B : Set β} :
                            a A a B A B
                            theorem Set.set_smul_subset_iff₀ {α : Type u_2} {β : Type u_3} [GroupWithZero α] [MulAction α β] {a : α} (ha : a 0) {A : Set β} {B : Set β} :
                            a A B A a⁻¹ B
                            theorem Set.subset_set_smul_iff₀ {α : Type u_2} {β : Type u_3} [GroupWithZero α] [MulAction α β] {a : α} (ha : a 0) {A : Set β} {B : Set β} :
                            A a B a⁻¹ A B
                            theorem Set.smul_set_inter₀ {α : Type u_2} {β : Type u_3} [GroupWithZero α] [MulAction α β] {s : Set β} {t : Set β} {a : α} (ha : a 0) :
                            a (s t) = a s a t
                            theorem Set.smul_set_sdiff₀ {α : Type u_2} {β : Type u_3} [GroupWithZero α] [MulAction α β] {s : Set β} {t : Set β} {a : α} (ha : a 0) :
                            a (s \ t) = a s \ a t
                            theorem Set.smul_set_symmDiff₀ {α : Type u_2} {β : Type u_3} [GroupWithZero α] [MulAction α β] {s : Set β} {t : Set β} {a : α} (ha : a 0) :
                            a symmDiff s t = symmDiff (a s) (a t)
                            theorem Set.smul_set_univ₀ {α : Type u_2} {β : Type u_3} [GroupWithZero α] [MulAction α β] {a : α} (ha : a 0) :
                            a Set.univ = Set.univ
                            theorem Set.smul_univ₀ {α : Type u_2} {β : Type u_3} [GroupWithZero α] [MulAction α β] {s : Set α} (hs : ¬s 0) :
                            s Set.univ = Set.univ
                            theorem Set.smul_univ₀' {α : Type u_2} {β : Type u_3} [GroupWithZero α] [MulAction α β] {s : Set α} (hs : s.Nontrivial) :
                            s Set.univ = Set.univ
                            @[simp]
                            theorem Set.inv_zero {α : Type u_2} [GroupWithZero α] :
                            0⁻¹ = 0
                            @[simp]
                            theorem Set.inv_smul_set_distrib₀ {α : Type u_2} [GroupWithZero α] (a : α) (s : Set α) :
                            @[simp]
                            theorem Set.inv_op_smul_set_distrib₀ {α : Type u_2} [GroupWithZero α] (a : α) (s : Set α) :
                            @[simp]
                            theorem Set.smul_set_neg {α : Type u_2} {β : Type u_3} [Monoid α] [AddGroup β] [DistribMulAction α β] (a : α) (t : Set β) :
                            a -t = -(a t)
                            @[simp]
                            theorem Set.smul_neg {α : Type u_2} {β : Type u_3} [Monoid α] [AddGroup β] [DistribMulAction α β] (s : Set α) (t : Set β) :
                            s -t = -(s t)
                            theorem Set.add_smul_subset {α : Type u_2} {β : Type u_3} [Semiring α] [AddCommMonoid β] [Module α β] (a : α) (b : α) (s : Set β) :
                            (a + b) s a s + b s
                            @[simp]
                            theorem Set.neg_smul_set {α : Type u_2} {β : Type u_3} [Ring α] [AddCommGroup β] [Module α β] (a : α) (t : Set β) :
                            -a t = -(a t)
                            @[simp]
                            theorem Set.neg_smul {α : Type u_2} {β : Type u_3} [Ring α] [AddCommGroup β] [Module α β] (s : Set α) (t : Set β) :
                            -s t = -(s t)