Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set

Set.smul_set_pi₀ theorem

 {M ι : Type*} {α : ι → Type*} [GroupWithZero M] [∀ i, MulAction M (α i)] {c : M} (hc : c ≠ 0) (I : Set ι)
  (s : ∀ i, Set (α i)) : c • I.pi s = I.pi (c • s)

Full source

lemma smul_set_pi₀ {M ι : Type*} {α : ι → Type*} [GroupWithZero M] [∀ i, MulAction M (α i)]
    {c : M} (hc : c ≠ 0) (I : Set ι) (s : ∀ i, Set (α i)) : c • I.pi s = I.pi (c • s) :=
  smul_set_pi_of_isUnit (.mk0 _ hc) I s

Scalar Multiplication Commutes with Product of Sets for Nonzero Elements in a Group with Zero

Informal description

Let $M$ be a group with zero acting on a family of types $\alpha_i$ for $i \in \iota$. For any nonzero element $c \in M$ (i.e., $c \neq 0$), any subset $I \subseteq \iota$, and any family of subsets $s_i \subseteq \alpha_i$ for $i \in I$, the scalar multiplication of $c$ on the product set $\prod_{i \in I} s_i$ is equal to the product of the scalar multiplications: $$c \cdot \prod_{i \in I} s_i = \prod_{i \in I} (c \cdot s_i).$$

Set.smul_set_pi₀' theorem

 {M ι : Type*} {α : ι → Type*} [GroupWithZero M] [∀ i, MulAction M (α i)] {c : M} {I : Set ι} (h : c ≠ 0 ∨ I = univ)
  (s : ∀ i, Set (α i)) : c • I.pi s = I.pi (c • s)

Full source

/-- A slightly more general version of `Set.smul_set_pi₀`. -/
lemma smul_set_pi₀' {M ι : Type*} {α : ι → Type*} [GroupWithZero M] [∀ i, MulAction M (α i)]
    {c : M} {I : Set ι} (h : c ≠ 0c ≠ 0 ∨ I = univ) (s : ∀ i, Set (α i)) : c • I.pi s = I.pi (c • s) :=
  h.elim (fun hc ↦ smul_set_pi_of_isUnit (.mk0 _ hc) I s) (fun hI ↦ hI ▸ smul_set_univ_pi ..)

Scalar Multiplication Commutes with Product of Sets for Nonzero Elements or Universal Index Set in a Group with Zero

Informal description

Let $M$ be a group with zero acting on a family of types $\alpha_i$ for $i \in \iota$. For any element $c \in M$ and any subset $I \subseteq \iota$, if either $c \neq 0$ or $I$ is the universal set, then the scalar multiplication of $c$ on the product set $\prod_{i \in I} s_i$ is equal to the product of the scalar multiplications: $$c \cdot \prod_{i \in I} s_i = \prod_{i \in I} (c \cdot s_i).$$

Set.smulZeroClassSet definition

[Zero β] [SMulZeroClass α β] : SMulZeroClass α (Set β)

Full source

/-- If scalar multiplication by elements of `α` sends `(0 : β)` to zero,
then the same is true for `(0 : Set β)`. -/
protected def smulZeroClassSet [Zero β] [SMulZeroClass α β] : SMulZeroClass α (Set β) where
  smul_zero _ := image_singleton.trans <| by rw [smul_zero, singleton_zero]

Scalar multiplication preserving zero on sets

Informal description

Given a type $\beta$ with a zero element and a scalar multiplication operation $\bullet$ between types $\alpha$ and $\beta$ that preserves zero (i.e., $a \bullet 0 = 0$ for any $a \in \alpha$), the structure `Set.smulZeroClassSet` defines a scalar multiplication operation on sets of $\beta$ that also preserves the zero set, i.e., $a \bullet \{0\} = \{0\}$ for any $a \in \alpha$.

Set.smul_zero_subset theorem

(s : Set α) : s • (0 : Set β) ⊆ 0

Full source

lemma smul_zero_subset (s : Set α) : s • (0 : Set β) ⊆ 0 := by simp [subset_def, mem_smul]

Pointwise scalar multiplication of a set with zero is contained in zero

Informal description

For any set $s$ of elements in a type $\alpha$, the pointwise scalar multiplication of $s$ with the zero set $\{0\}$ in a type $\beta$ is a subset of the zero set $\{0\}$ in $\beta$, i.e., $s \cdot \{0\} \subseteq \{0\}$.

Set.Nonempty.smul_zero theorem

(hs : s.Nonempty) : s • (0 : Set β) = 0

Full source

lemma Nonempty.smul_zero (hs : s.Nonempty) : s • (0 : Set β) = 0 :=
  s.smul_zero_subset.antisymm <| by simpa [mem_smul] using hs

Nonempty Set Scalar Multiplication with Zero Yields Zero

Informal description

For any nonempty set $s$ of elements in a type $\alpha$, the pointwise scalar multiplication of $s$ with the zero set $\{0\}$ in a type $\beta$ equals the zero set $\{0\}$ in $\beta$, i.e., $s \cdot \{0\} = \{0\}$.

Set.zero_mem_smul_set theorem

(h : (0 : β) ∈ t) : (0 : β) ∈ a • t

Full source

lemma zero_mem_smul_set (h : (0 : β) ∈ t) : (0 : β) ∈ a • t := ⟨0, h, smul_zero _⟩

Zero Preservation under Scalar Multiplication of Sets

Informal description

For any scalar $a$ and any set $t$ in a type $\beta$ with a zero element, if $0 \in t$, then $0 \in a \cdot t$, where $a \cdot t$ denotes the scalar multiplication of $a$ with each element of $t$.

Set.zero_mem_smul_set_iff theorem

(ha : a ≠ 0) : (0 : β) ∈ a • t ↔ (0 : β) ∈ t

Full source

lemma zero_mem_smul_set_iff (ha : a ≠ 0) : (0 : β) ∈ a • t(0 : β) ∈ a • t ↔ (0 : β) ∈ t := by
  refine ⟨?_, zero_mem_smul_set⟩
  rintro ⟨b, hb, h⟩
  rwa [(eq_zero_or_eq_zero_of_smul_eq_zero h).resolve_left ha] at hb

Zero Membership in Scalar Multiplication of Sets for Nonzero Scalars

Informal description

For any nonzero scalar $a$ and any set $t$ in a type $\beta$ with a zero element, the zero element is in the scalar multiplication $a \cdot t$ if and only if the zero element is in $t$. That is, $0 \in a \cdot t \leftrightarrow 0 \in t$.

Set.zero_smul_subset theorem

(t : Set β) : (0 : Set α) • t ⊆ 0

Full source

lemma zero_smul_subset (t : Set β) : (0 : Set α) • t ⊆ 0 := by simp [subset_def, mem_smul]

Zero Set Scalar Multiplication Subset Property: $\{0\} \cdot t \subseteq \{0\}$

Informal description

For any set $t$ in a type $\beta$ with a zero element, the pointwise scalar multiplication of the zero set $\{0\}$ in $\alpha$ with $t$ is a subset of the zero set $\{0\}$ in $\beta$, i.e., $\{0\} \cdot t \subseteq \{0\}$.

Set.Nonempty.zero_smul theorem

(ht : t.Nonempty) : (0 : Set α) • t = 0

Full source

lemma Nonempty.zero_smul (ht : t.Nonempty) : (0 : Set α) • t = 0 :=
  t.zero_smul_subset.antisymm <| by simpa [mem_smul] using ht

Zero Set Scalar Multiplication of Nonempty Set Yields Zero Set: $\{0\} \cdot t = \{0\}$ for $t$ nonempty

Informal description

For any nonempty set $t$ in a type $\beta$ with a zero element, the pointwise scalar multiplication of the zero set $\{0\}$ in $\alpha$ with $t$ equals the zero set $\{0\}$ in $\beta$, i.e., $\{0\} \cdot t = \{0\}$.

Set.zero_smul_set theorem

{s : Set β} (h : s.Nonempty) : (0 : α) • s = (0 : Set β)

Full source

/-- A nonempty set is scaled by zero to the singleton set containing 0. -/
@[simp] lemma zero_smul_set {s : Set β} (h : s.Nonempty) : (0 : α) • s = (0 : Set β) := by
  simp only [← image_smul, image_eta, zero_smul, h.image_const, singleton_zero]

Scalar Multiplication of Nonempty Set by Zero Yields Singleton Zero: $0 \cdot s = \{0\}$

Informal description

For any nonempty set $s \subseteq \beta$ and a scalar multiplication operation $\cdot$ between types $\alpha$ and $\beta$, the scalar multiplication of $0 \in \alpha$ with $s$ equals the singleton set $\{0\}$ in $\beta$, i.e., $0 \cdot s = \{0\}$.

Set.zero_smul_set_subset theorem

(s : Set β) : (0 : α) • s ⊆ 0

Full source

lemma zero_smul_set_subset (s : Set β) : (0 : α) • s ⊆ 0 :=
  image_subset_iff.2 fun x _ ↦ zero_smul α x

Scalar Multiplication by Zero Yields Subset of Zero: $0 \cdot s \subseteq \{0\}$

Informal description

For any set $s \subseteq \beta$, the scalar multiplication of $0 \in \alpha$ with $s$ is a subset of the singleton set $\{0\}$ in $\beta$, i.e., $0 \cdot s \subseteq \{0\}$.

Set.subsingleton_zero_smul_set theorem

(s : Set β) : ((0 : α) • s).Subsingleton

Full source

lemma subsingleton_zero_smul_set (s : Set β) : ((0 : α) • s).Subsingleton :=
  subsingleton_singleton.anti <| zero_smul_set_subset s

Subsingleton Property of Zero Scalar Multiplication: $(0 \cdot s)$ is a subsingleton

Informal description

For any set $s \subseteq \beta$, the scalar multiplication of $0 \in \alpha$ with $s$ results in a subsingleton set, i.e., the set $\{0 \cdot y \mid y \in s\}$ contains at most one element.

Set.zero_mem_smul_iff theorem

: 0 ∈ s • t ↔ 0 ∈ s ∧ t.Nonempty ∨ 0 ∈ t ∧ s.Nonempty

Full source

lemma zero_mem_smul_iff : 0 ∈ s • t0 ∈ s • t ↔ 0 ∈ s ∧ t.Nonempty ∨ 0 ∈ t ∧ s.Nonempty where
  mp := by
    rintro ⟨a, ha, b, hb, h⟩
    obtain rfl | rfl := eq_zero_or_eq_zero_of_smul_eq_zero h
    · exact Or.inl ⟨ha, b, hb⟩
    · exact Or.inr ⟨hb, a, ha⟩
  mpr := by
    rintro (⟨hs, b, hb⟩ | ⟨ht, a, ha⟩)
    · exact ⟨0, hs, b, hb, zero_smul _ _⟩
    · exact ⟨a, ha, 0, ht, smul_zero _⟩

Zero Membership in Pointwise Product of Sets: $0 \in s \cdot t$ iff ($0 \in s$ and $t$ nonempty) or ($0 \in t$ and $s$ nonempty)

Informal description

For sets $s$ and $t$ with a scalar multiplication operation, the zero element $0$ belongs to the pointwise product $s \cdot t$ if and only if either $0 \in s$ and $t$ is nonempty, or $0 \in t$ and $s$ is nonempty.

Set.distribSMulSet definition

[AddZeroClass β] [DistribSMul α β] : DistribSMul α (Set β)

Full source

/-- If the scalar multiplication `(· • ·) : α → β → β` is distributive,
then so is `(· • ·) : α → Set β → Set β`. -/
protected def distribSMulSet [AddZeroClass β] [DistribSMul α β] : DistribSMul α (Set β) where
  smul_add _ _ _ := image_image2_distrib <| smul_add _

Distributive scalar multiplication on sets

Informal description

Given an additive monoid $\beta$ and a scalar multiplication operation $\bullet$ between types $\alpha$ and $\beta$ that is right-distributive over addition (i.e., $a \bullet (b_1 + b_2) = a \bullet b_1 + a \bullet b_2$ for all $a \in \alpha$ and $b_1, b_2 \in \beta$), the structure `Set.distribSMulSet` defines a scalar multiplication operation on sets of $\beta$ that preserves set addition (i.e., $a \bullet (s_1 + s_2) = a \bullet s_1 + a \bullet s_2$ for any $a \in \alpha$ and sets $s_1, s_2 \subseteq \beta$).

Set.distribMulActionSet definition

[Monoid α] [AddMonoid β] [DistribMulAction α β] : DistribMulAction α (Set β)

Full source

/-- A distributive multiplicative action of a monoid on an additive monoid `β` gives a distributive
multiplicative action on `Set β`. -/
protected def distribMulActionSet [Monoid α] [AddMonoid β] [DistribMulAction α β] :
    DistribMulAction α (Set β) where
  smul_add := smul_add
  smul_zero := smul_zero

Pointwise distributive multiplicative action on sets

Informal description

Given a monoid $\alpha$ and an additive monoid $\beta$ with a distributive multiplicative action of $\alpha$ on $\beta$, this defines a distributive multiplicative action of $\alpha$ on the power set $\mathcal{P}(\beta)$. The action is defined pointwise, satisfying $a \cdot (s + t) = a \cdot s + a \cdot t$ and $a \cdot \emptyset = \emptyset$ for all $a \in \alpha$ and subsets $s, t \subseteq \beta$.

Set.mulDistribMulActionSet definition

[Monoid α] [Monoid β] [MulDistribMulAction α β] : MulDistribMulAction α (Set β)

Full source

/-- A multiplicative action of a monoid on a monoid `β` gives a multiplicative action on `Set β`. -/
protected def mulDistribMulActionSet [Monoid α] [Monoid β] [MulDistribMulAction α β] :
    MulDistribMulAction α (Set β) where
  smul_mul _ _ _ := image_image2_distrib <| smul_mul' _
  smul_one _ := image_singleton.trans <| by rw [smul_one, singleton_one]

Pointwise multiplicative distributive action on power sets

Informal description

Given a monoid $\alpha$ acting distributively on a monoid $\beta$, this defines a multiplicative distributive action of $\alpha$ on the power set $\mathcal{P}(\beta)$ (the set of all subsets of $\beta$). The action is defined by pointwise multiplication: for $a \in \alpha$ and $S \subseteq \beta$, the action $a \cdot S$ is the set $\{a \cdot x \mid x \in S\}$. This action preserves the multiplicative structure, meaning that for any $a \in \alpha$ and subsets $S, T \subseteq \beta$, we have $a \cdot (S * T) = (a \cdot S) * (a \cdot T)$, where $*$ denotes the pointwise product of sets.

Set.instNoZeroSMulDivisors instance

[Zero α] [Zero β] [SMul α β] [NoZeroSMulDivisors α β] : NoZeroSMulDivisors (Set α) (Set β)

Full source

instance instNoZeroSMulDivisors [Zero α] [Zero β] [SMul α β] [NoZeroSMulDivisors α β] :
    NoZeroSMulDivisors (Set α) (Set β) where
  eq_zero_or_eq_zero_of_smul_eq_zero {s t} h := by
    by_contra! H
    have hst : (s • t).Nonempty := h.symm.subst zero_nonempty
    rw [Ne, ← hst.of_smul_left.subset_zero_iff, Ne,
      ← hst.of_smul_right.subset_zero_iff] at H
    simp only [not_subset, mem_zero] at H
    obtain ⟨⟨a, hs, ha⟩, b, ht, hb⟩ := H
    exact (eq_zero_or_eq_zero_of_smul_eq_zero <| h.subset <| smul_mem_smul hs ht).elim ha hb

No Zero Scalar Divisors Property for Pointwise Set Multiplication

Informal description

For any types $\alpha$ and $\beta$ with zero elements and a scalar multiplication operation $\bullet : \alpha \to \beta \to \beta$, if $\alpha$ and $\beta$ satisfy the no-zero-smul-divisors property (i.e., $a \bullet b = 0$ implies $a = 0$ or $b = 0$), then the pointwise scalar multiplication on sets $\mathcal{P}(\alpha)$ and $\mathcal{P}(\beta)$ also satisfies the no-zero-smul-divisors property.

Set.noZeroSMulDivisors_set instance

[Zero α] [Zero β] [SMul α β] [NoZeroSMulDivisors α β] : NoZeroSMulDivisors α (Set β)

Full source

instance noZeroSMulDivisors_set [Zero α] [Zero β] [SMul α β] [NoZeroSMulDivisors α β] :
    NoZeroSMulDivisors α (Set β) where
  eq_zero_or_eq_zero_of_smul_eq_zero {a s} h := by
    by_contra! H
    have hst : (a • s).Nonempty := h.symm.subst zero_nonempty
    rw [Ne, Ne, ← hst.of_image.subset_zero_iff, not_subset] at H
    obtain ⟨ha, b, ht, hb⟩ := H
    exact (eq_zero_or_eq_zero_of_smul_eq_zero <| h.subset <| smul_mem_smul_set ht).elim ha hb

No Zero Divisors Between Scalar Type and Power Set of Target Type

Informal description

For types $\alpha$ and $\beta$ with zero elements and a scalar multiplication operation $\cdot : \alpha \to \beta \to \beta$, if $\alpha$ and $\beta$ have no zero divisors with respect to this scalar multiplication, then $\alpha$ and the power set of $\beta$ also have no zero divisors. In other words, for any nonzero $a \in \alpha$ and any nonempty subset $A \subseteq \beta$, the scaled set $a \cdot A$ is nonempty.

Set.instNoZeroDivisors instance

[Zero α] [Mul α] [NoZeroDivisors α] : NoZeroDivisors (Set α)

Full source

instance [Zero α] [Mul α] [NoZeroDivisors α] : NoZeroDivisors (Set α) where
  eq_zero_or_eq_zero_of_mul_eq_zero h := eq_zero_or_eq_zero_of_smul_eq_zero h

No Zero Divisors for Pointwise Set Multiplication

Informal description

For any type $\alpha$ with a zero element and a multiplication operation that has no zero divisors, the pointwise multiplication operation on sets of $\alpha$ also has no zero divisors. That is, for any sets $A, B \subseteq \alpha$, if $A * B = \{0\}$, then either $A = \{0\}$ or $B = \{0\}$.

Set.smul_mem_smul_set_iff₀ theorem

(ha : a ≠ 0) (A : Set β) (x : β) : a • x ∈ a • A ↔ x ∈ A

Full source

@[simp]
lemma smul_mem_smul_set_iff₀ (ha : a ≠ 0) (A : Set β) (x : β) : a • x ∈ a • Aa • x ∈ a • A ↔ x ∈ A :=
  show Units.mk0Units.mk0 a ha • _ ∈ _Units.mk0 a ha • _ ∈ _ ↔ _ from smul_mem_smul_set_iff

Membership in scaled set for nonzero scalars: $a \cdot x \in a \cdot A \leftrightarrow x \in A$

Informal description

Let $G_0$ be a group with zero acting on a type $\beta$, and let $a \in G_0$ be a nonzero element. For any subset $A \subseteq \beta$ and any element $x \in \beta$, the element $a \cdot x$ belongs to the scaled set $a \cdot A$ if and only if $x$ belongs to $A$.

Set.mem_smul_set_iff_inv_smul_mem₀ theorem

(ha : a ≠ 0) (A : Set β) (x : β) : x ∈ a • A ↔ a⁻¹ • x ∈ A

Full source

lemma mem_smul_set_iff_inv_smul_mem₀ (ha : a ≠ 0) (A : Set β) (x : β) : x ∈ a • Ax ∈ a • A ↔ a⁻¹ • x ∈ A :=
  show _ ∈ Units.mk0 a ha • __ ∈ Units.mk0 a ha • _ ↔ _ from mem_smul_set_iff_inv_smul_mem

Characterization of membership in scaled set via inverse action in a group with zero: $x \in a \cdot A \leftrightarrow a^{-1} \cdot x \in A$ for $a \neq 0$

Informal description

Let $G_0$ be a group with zero acting on a type $\beta$, and let $a \in G_0$ be a nonzero element. For any subset $A \subseteq \beta$ and any element $x \in \beta$, we have: \[ x \in a \cdot A \leftrightarrow a^{-1} \cdot x \in A. \]

Set.mem_inv_smul_set_iff₀ theorem

(ha : a ≠ 0) (A : Set β) (x : β) : x ∈ a⁻¹ • A ↔ a • x ∈ A

Full source

lemma mem_inv_smul_set_iff₀ (ha : a ≠ 0) (A : Set β) (x : β) : x ∈ a⁻¹ • Ax ∈ a⁻¹ • A ↔ a • x ∈ A :=
  show _ ∈ (Units.mk0 a ha)⁻¹ • __ ∈ (Units.mk0 a ha)⁻¹ • _ ↔ _ from mem_inv_smul_set_iff

Characterization of membership in inversely scaled set for nonzero elements: $x \in a^{-1} \cdot A \leftrightarrow a \cdot x \in A$

Informal description

Let $G_0$ be a group with zero acting on a type $\beta$, and let $a \in G_0$ be a nonzero element. For any subset $A \subseteq \beta$ and any element $x \in \beta$, we have: \[ x \in a^{-1} \cdot A \leftrightarrow a \cdot x \in A. \]

Set.preimage_smul₀ theorem

(ha : a ≠ 0) (t : Set β) : (fun x ↦ a • x) ⁻¹' t = a⁻¹ • t

Full source

lemma preimage_smul₀ (ha : a ≠ 0) (t : Set β) : (fun x ↦ a • x) ⁻¹' t = a⁻¹ • t :=
  preimage_smul (Units.mk0 a ha) t

Preimage of Scalar Multiplication by Nonzero Element Equals Inverse Scalar Multiplication of Set

Informal description

Let $G_0$ be a group with zero acting on a type $\beta$, and let $a \in G_0$ be a nonzero element. For any subset $t \subseteq \beta$, the preimage of $t$ under the left scalar multiplication by $a$ is equal to the left scalar multiplication of $t$ by $a^{-1}$, i.e., \[ \{x \in \beta \mid a \cdot x \in t\} = a^{-1} \cdot t. \]

Set.preimage_smul_inv₀ theorem

(ha : a ≠ 0) (t : Set β) : (fun x ↦ a⁻¹ • x) ⁻¹' t = a • t

Full source

lemma preimage_smul_inv₀ (ha : a ≠ 0) (t : Set β) : (fun x ↦ a⁻¹ • x) ⁻¹' t = a • t :=
  preimage_smul (Units.mk0 a ha)⁻¹ t

Preimage of Inverse Scalar Multiplication Equals Scalar Multiplication of Set in Group with Zero

Informal description

Let $G_0$ be a group with zero acting on a type $\beta$, and let $a \in G_0$ be a nonzero element. For any subset $t \subseteq \beta$, the preimage of $t$ under the scalar multiplication by $a^{-1}$ is equal to the scalar multiplication of $t$ by $a$, i.e., \[ \{x \in \beta \mid a^{-1} \cdot x \in t\} = a \cdot t. \]

Set.smul_set_subset_smul_set_iff₀ theorem

(ha : a ≠ 0) {A B : Set β} : a • A ⊆ a • B ↔ A ⊆ B

Full source

@[simp]
lemma smul_set_subset_smul_set_iff₀ (ha : a ≠ 0) {A B : Set β} : a • A ⊆ a • Ba • A ⊆ a • B ↔ A ⊆ B :=
  show Units.mk0Units.mk0 a ha • _ ⊆ _Units.mk0 a ha • _ ⊆ _ ↔ _ from smul_set_subset_smul_set_iff

Scalar Multiplication Preserves Subset Relation for Nonzero Elements: $a \cdot A \subseteq a \cdot B \leftrightarrow A \subseteq B$

Informal description

Let $G_0$ be a group with zero, and let $a \in G_0$ be a nonzero element. For any subsets $A, B$ of a type $\beta$ with a multiplicative action by $G_0$, the subset relation $a \cdot A \subseteq a \cdot B$ holds if and only if $A \subseteq B$.

Set.smul_set_subset_iff₀ theorem

(ha : a ≠ 0) {A B : Set β} : a • A ⊆ B ↔ A ⊆ a⁻¹ • B

Full source

lemma smul_set_subset_iff₀ (ha : a ≠ 0) {A B : Set β} : a • A ⊆ Ba • A ⊆ B ↔ A ⊆ a⁻¹ • B :=
  show Units.mk0Units.mk0 a ha • _ ⊆ _Units.mk0 a ha • _ ⊆ _ ↔ _ from smul_set_subset_iff_subset_inv_smul_set

Subset relation under scalar multiplication in a group with zero: $a \cdot A \subseteq B \leftrightarrow A \subseteq a^{-1} \cdot B$

Informal description

Let $G_0$ be a group with zero acting on a type $\beta$, and let $a \in G_0$ be a nonzero element. For any subsets $A, B \subseteq \beta$, the following equivalence holds: \[ a \cdot A \subseteq B \quad \text{if and only if} \quad A \subseteq a^{-1} \cdot B. \] Here, $a \cdot A$ denotes the set $\{a \cdot x \mid x \in A\}$ and $a^{-1} \cdot B$ denotes the set $\{a^{-1} \cdot y \mid y \in B\}$.

Set.subset_smul_set_iff₀ theorem

(ha : a ≠ 0) {A B : Set β} : A ⊆ a • B ↔ a⁻¹ • A ⊆ B

Full source

lemma subset_smul_set_iff₀ (ha : a ≠ 0) {A B : Set β} : A ⊆ a • BA ⊆ a • B ↔ a⁻¹ • A ⊆ B :=
  show _ ⊆ Units.mk0 a ha • __ ⊆ Units.mk0 a ha • _ ↔ _ from subset_smul_set_iff

Subset relation under scalar multiplication by a nonzero element: $A \subseteq a \cdot B \leftrightarrow a^{-1} \cdot A \subseteq B$

Informal description

Let $G_0$ be a group with zero acting on a type $\beta$, and let $a \in G_0$ be a nonzero element. For any subsets $A, B \subseteq \beta$, we have $A \subseteq a \cdot B$ if and only if $a^{-1} \cdot A \subseteq B$.

Set.smul_set_inter₀ theorem

(ha : a ≠ 0) : a • (s ∩ t) = a • s ∩ a • t

Full source

lemma smul_set_inter₀ (ha : a ≠ 0) : a • (s ∩ t) = a • s ∩ a • t :=
  show Units.mk0 a ha • _ = _ from smul_set_inter

Scalar Multiplication Distributes Over Set Intersection for Nonzero Elements: $a \cdot (s \cap t) = (a \cdot s) \cap (a \cdot t)$

Informal description

For any nonzero element $a$ in a group with zero $G_0$, and any two sets $s$ and $t$ in a type $\beta$ with a multiplicative action by $G_0$, the scalar multiplication of $a$ on the intersection $s \cap t$ is equal to the intersection of the scalar multiplications of $a$ on $s$ and $t$, i.e., $a \cdot (s \cap t) = (a \cdot s) \cap (a \cdot t)$.

Set.smul_set_sdiff₀ theorem

(ha : a ≠ 0) : a • (s \ t) = a • s \ a • t

Full source

lemma smul_set_sdiff₀ (ha : a ≠ 0) : a • (s \ t) = a • s \ a • t :=
  image_diff (MulAction.injective₀ ha) _ _

Scalar Multiplication Preserves Set Difference for Nonzero Elements: $a \cdot (s \setminus t) = (a \cdot s) \setminus (a \cdot t)$

Informal description

For any nonzero element $a$ in a group with zero acting on a type $\beta$, and any subsets $s, t \subseteq \beta$, the scalar multiplication of $a$ on the set difference $s \setminus t$ is equal to the set difference of the scalar multiplications of $a$ on $s$ and $t$, i.e., $$ a \cdot (s \setminus t) = (a \cdot s) \setminus (a \cdot t). $$

Set.smul_set_symmDiff₀ theorem

(ha : a ≠ 0) : a • s ∆ t = (a • s) ∆ (a • t)

Full source

lemma smul_set_symmDiff₀ (ha : a ≠ 0) : a • s ∆ t = (a • s) ∆ (a • t) :=
  image_symmDiff (MulAction.injective₀ ha) _ _

Scalar Multiplication Preserves Symmetric Difference for Nonzero Elements: $a \cdot (s \triangle t) = (a \cdot s) \triangle (a \cdot t)$

Informal description

For any nonzero element $a$ in a group with zero acting on a type $\beta$, and any subsets $s, t \subseteq \beta$, the scalar multiplication of $a$ on the symmetric difference $s \triangle t$ is equal to the symmetric difference of the scalar multiplications of $a$ on $s$ and $t$, i.e., $$ a \cdot (s \triangle t) = (a \cdot s) \triangle (a \cdot t). $$

Set.smul_set_univ₀ theorem

(ha : a ≠ 0) : a • (univ : Set β) = univ

Full source

lemma smul_set_univ₀ (ha : a ≠ 0) : a • (univ : Set β) = univ :=
  image_univ_of_surjective <| MulAction.surjective₀ ha

Universal Set Preservation under Nonzero Scalar Multiplication

Informal description

For any nonzero element $a$ in a group with zero acting on a type $\beta$, the scalar multiplication of $a$ with the universal set $\text{univ} \subseteq \beta$ equals $\text{univ}$, i.e., $a \bullet \text{univ} = \text{univ}$.

Set.smul_univ₀ theorem

{s : Set α} (hs : ¬s ⊆ 0) : s • (univ : Set β) = univ

Full source

lemma smul_univ₀ {s : Set α} (hs : ¬s ⊆ 0) : s • (univ : Set β) = univ :=
  let ⟨a, ha, ha₀⟩ := not_subset.1 hs
  eq_univ_of_forall fun b ↦ ⟨a, ha, a⁻¹ • b, trivial, smul_inv_smul₀ ha₀ _⟩

Pointwise Scalar Multiplication of Nonzero Set with Universal Set Yields Universal Set

Informal description

For any set $s$ of elements in a group with zero $\alpha$ that is not a subset of $\{0\}$, the pointwise scalar multiplication of $s$ with the universal set $\text{univ} : \text{Set} \beta$ equals $\text{univ}$, i.e., $s \bullet \text{univ} = \text{univ}$.

Set.smul_univ₀' theorem

{s : Set α} (hs : s.Nontrivial) : s • (univ : Set β) = univ

Full source

lemma smul_univ₀' {s : Set α} (hs : s.Nontrivial) : s • (univ : Set β) = univ :=
  smul_univ₀ hs.not_subset_singleton

Nontrivial Set Scalar Multiplication with Universal Set Yields Universal Set

Informal description

For any nontrivial subset $s$ of a group with zero $\alpha$, the pointwise scalar multiplication of $s$ with the universal set $\text{univ} \subseteq \beta$ equals $\text{univ}$, i.e., $s \bullet \text{univ} = \text{univ}$.

Set.inv_smul_set_distrib₀ theorem

(a : α) (s : Set α) : (a • s)⁻¹ = s⁻¹ <• a⁻¹

Full source

@[simp] lemma inv_smul_set_distrib₀ (a : α) (s : Set α) : (a • s)⁻¹ = s⁻¹s⁻¹ <• a⁻¹ := by
  obtain rfl | ha := eq_or_ne a 0
  · obtain rfl | hs := s.eq_empty_or_nonempty <;> simp [*]
  · ext; simp [mem_smul_set_iff_inv_smul_mem₀, *]

Inverse of Dilation Equals Opposite Dilation of Inverses: $(a \cdot s)^{-1} = s^{-1} \cdot_{\text{op}} a^{-1}$

Informal description

For any element $a$ in a group with zero $\alpha$ and any subset $s$ of $\alpha$, the pointwise inverse of the dilation of $s$ by $a$ equals the dilation of the pointwise inverse of $s$ by the inverse of $a$ in the opposite multiplicative structure, i.e., $(a \cdot s)^{-1} = s^{-1} \cdot_{\text{op}} a^{-1}$.

Set.inv_op_smul_set_distrib₀ theorem

(a : α) (s : Set α) : (s <• a)⁻¹ = a⁻¹ • s⁻¹

Full source

@[simp] lemma inv_op_smul_set_distrib₀ (a : α) (s : Set α) : (s <• a)⁻¹ = a⁻¹ • s⁻¹ := by
  obtain rfl | ha := eq_or_ne a 0
  · obtain rfl | hs := s.eq_empty_or_nonempty <;> simp [*]
  · ext; simp [mem_smul_set_iff_inv_smul_mem₀, *]

Inverse of Right Scalar Multiplication Equals Left Scalar Multiplication of Inverses in a Group with Zero

Informal description

Let $\alpha$ be a group with zero. For any element $a \in \alpha$ and any subset $s \subseteq \alpha$, the pointwise inverse of the right scalar multiplication $s \bullet a$ equals the left scalar multiplication of the inverse of $a$ with the pointwise inverse of $s$, i.e., $(s \bullet a)^{-1} = a^{-1} \bullet s^{-1}$.

Tags