Mathlib.Algebra.Group.Pointwise.Set.Basic

Set.one definition

: One (Set α)

Full source

/-- The set `1 : Set α` is defined as `{1}` in locale `Pointwise`. -/
@[to_additive "The set `0 : Set α` is defined as `{0}` in locale `Pointwise`."]
protected noncomputable def one : One (Set α) :=
  ⟨{1}⟩

Multiplicative identity set

Informal description

The set `1 : Set α` is defined as the singleton set containing the multiplicative identity element `{1}` in the locale `Pointwise`.

Set.singleton_one theorem

: ({ 1 } : Set α) = 1

Full source

@[to_additive]
theorem singleton_one : ({1} : Set α) = 1 :=
  rfl

Singleton of One Equals Multiplicative Identity Set

Informal description

For a type $\alpha$ with a multiplicative identity element $1$, the singleton set $\{1\}$ is equal to the multiplicative identity set $1$ in the context of pointwise operations on sets.

Set.mem_one theorem

: a ∈ (1 : Set α) ↔ a = 1

Full source

@[to_additive (attr := simp)]
theorem mem_one : a ∈ (1 : Set α)a ∈ (1 : Set α) ↔ a = 1 :=
  Iff.rfl

Characterization of Membership in Multiplicative Identity Set

Informal description

For any element $a$ of type $\alpha$, $a$ belongs to the multiplicative identity set $1$ if and only if $a$ is equal to the multiplicative identity element $1$ of $\alpha$.

Set.one_mem_one theorem

: (1 : α) ∈ (1 : Set α)

Full source

@[to_additive]
theorem one_mem_one : (1 : α) ∈ (1 : Set α) :=
  Eq.refl _

Multiplicative Identity Belongs to Its Singleton Set

Informal description

The multiplicative identity element $1$ of type $\alpha$ is contained in the singleton set $\{1\}$ of type $\alpha$.

Set.one_subset theorem

: 1 ⊆ s ↔ (1 : α) ∈ s

Full source

@[to_additive (attr := simp)]
theorem one_subset : 1 ⊆ s1 ⊆ s ↔ (1 : α) ∈ s :=
  singleton_subset_iff

Subset Criterion for Multiplicative Identity Set: $\{1\} \subseteq s \leftrightarrow 1 \in s$

Informal description

For any set $s$ over a type $\alpha$ with a multiplicative identity element $1$, the singleton set $\{1\}$ is a subset of $s$ if and only if $1$ is an element of $s$.

Set.one_nonempty theorem

: (1 : Set α).Nonempty

Full source

@[to_additive (attr := simp)]
theorem one_nonempty : (1 : Set α).Nonempty :=
  ⟨1, rfl⟩

Nonemptiness of the Multiplicative Identity Set

Informal description

The singleton set $\{1\}$ containing the multiplicative identity element in a type $\alpha$ is nonempty.

Set.image_one theorem

{f : α → β} : f '' 1 = {f 1}

Full source

@[to_additive (attr := simp)]
theorem image_one {f : α → β} : f '' 1 = {f 1} :=
  image_singleton

Image of Multiplicative Identity Set is Singleton of Function Value at One

Informal description

For any function $f : \alpha \to \beta$, the image of the multiplicative identity set $\{1\}$ under $f$ is the singleton set $\{f(1)\}$.

Set.subset_one_iff_eq theorem

: s ⊆ 1 ↔ s = ∅ ∨ s = 1

Full source

@[to_additive]
theorem subset_one_iff_eq : s ⊆ 1s ⊆ 1 ↔ s = ∅ ∨ s = 1 :=
  subset_singleton_iff_eq

Subset Characterization of Multiplicative Identity Set: $s \subseteq \{1\} \leftrightarrow s = \emptyset \lor s = \{1\}$

Informal description

For any set $s$ over a type $\alpha$ with a multiplicative identity element $1$, the set $s$ is a subset of the singleton $\{1\}$ if and only if $s$ is either the empty set or the singleton $\{1\}$ itself.

Set.Nonempty.subset_one_iff theorem

(h : s.Nonempty) : s ⊆ 1 ↔ s = 1

Full source

@[to_additive]
theorem Nonempty.subset_one_iff (h : s.Nonempty) : s ⊆ 1s ⊆ 1 ↔ s = 1 :=
  h.subset_singleton_iff

Nonempty Subset of Singleton Identity Set Characterization: $s \subseteq \{1\} \leftrightarrow s = \{1\}$

Informal description

For any nonempty set $s$ over a type $\alpha$ with a multiplicative identity element $1$, the set $s$ is a subset of the singleton $\{1\}$ if and only if $s$ is equal to $\{1\}$.

Set.singletonOneHom definition

: OneHom α (Set α)

Full source

/-- The singleton operation as a `OneHom`. -/
@[to_additive "The singleton operation as a `ZeroHom`."]
noncomputable def singletonOneHom : OneHom α (Set α) where
  toFun := singleton; map_one' := singleton_one

Singleton set homomorphism preserving identity

Informal description

The function that maps an element $a$ of a type $\alpha$ with a multiplicative identity element $1$ to the singleton set $\{a\}$ is a homomorphism preserving the identity, i.e., it maps $1$ to $\{1\}$.

Set.coe_singletonOneHom theorem

: (singletonOneHom : α → Set α) = singleton

Full source

@[to_additive (attr := simp)]
theorem coe_singletonOneHom : (singletonOneHom : α → Set α) = singleton :=
  rfl

Equality of Singleton Set Homomorphism and Singleton Constructor

Informal description

The function `singletonOneHom`, which maps an element $a$ of a type $\alpha$ with a multiplicative identity to the singleton set $\{a\}$, is equal to the standard singleton set constructor function `singleton`.

Set.image_op_one theorem

: (1 : Set α).image op = 1

Full source

@[to_additive] lemma image_op_one : (1 : Set α).image op = 1 := image_singleton

Image of Identity Set under Opposite Embedding Equals Identity Set

Informal description

For any type $\alpha$ with a multiplicative identity element $1$, the image of the singleton set $\{1\}$ under the canonical embedding $\text{op} : \alpha \to \alpha^\text{op}$ is equal to the singleton set $\{1\}$ in the multiplicative opposite $\alpha^\text{op}$.

Set.one_prod_one theorem

[One β] : (1 ×ˢ 1 : Set (α × β)) = 1

Full source

@[to_additive (attr := simp) zero_prod_zero]
lemma one_prod_one [One β] : (1 ×ˢ 1 : Set (α × β)) = 1 := by ext; simp [Prod.ext_iff]

Cartesian Product of Identity Sets Equals Identity Set

Informal description

For any types $\alpha$ and $\beta$ each equipped with a multiplicative identity element, the Cartesian product of the singleton sets $\{1\} \subseteq \alpha$ and $\{1\} \subseteq \beta$ equals the singleton set $\{1\} \subseteq \alpha \times \beta$, i.e., $\{1\} \timesˢ \{1\} = \{1\}$.

Set.inv definition

[Inv α] : Inv (Set α)

Full source

/-- 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_eq_inv`. -/
@[to_additive
      "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_eq_neg`."]
protected def inv [Inv α] : Inv (Set α) :=
  ⟨preimage Inv.inv⟩

Pointwise inversion of a set

Informal description

The pointwise inversion of a set $s$ in a type $\alpha$ equipped with an inversion operation is defined as the set $\{x \mid x^{-1} \in s\}$. This is equivalent to the image of $s$ under the inversion operation, $\{x^{-1} \mid x \in s\}$.

Set.mem_inv theorem

: a ∈ s⁻¹ ↔ a⁻¹ ∈ s

Full source

@[to_additive (attr := simp)]
theorem mem_inv : a ∈ s⁻¹a ∈ s⁻¹ ↔ a⁻¹ ∈ s :=
  Iff.rfl

Characterization of Membership in Pointwise Inverse Set

Informal description

For any element $a$ in a type $\alpha$ with an inversion operation and any set $s \subseteq \alpha$, the element $a$ belongs to the pointwise inverse set $s^{-1}$ if and only if its inverse $a^{-1}$ belongs to $s$. In symbols: \[ a \in s^{-1} \leftrightarrow a^{-1} \in s. \]

Set.inv_preimage theorem

: Inv.inv ⁻¹' s = s⁻¹

Full source

@[to_additive (attr := simp)]
theorem inv_preimage : Inv.invInv.inv ⁻¹' s = s⁻¹ :=
  rfl

Preimage of Inversion Equals Pointwise Inversion of Set

Informal description

For any set $s$ in a type $\alpha$ equipped with an inversion operation, the preimage of $s$ under the inversion function equals the pointwise inversion of $s$, i.e., $\text{Inv.inv}^{-1}(s) = s^{-1}$.

Set.inv_empty theorem

: (∅ : Set α)⁻¹ = ∅

Full source

@[to_additive (attr := simp)]
theorem inv_empty : (∅ : Set α)⁻¹ = ∅ :=
  rfl

Inversion of Empty Set is Empty

Informal description

For any type $\alpha$ equipped with an inversion operation, the pointwise inversion of the empty set is the empty set, i.e., $\emptyset^{-1} = \emptyset$.

Set.inv_univ theorem

: (univ : Set α)⁻¹ = univ

Full source

@[to_additive (attr := simp)]
theorem inv_univ : (univ : Set α)⁻¹ = univ :=
  rfl

Inversion Preserves the Universal Set

Informal description

For any type $\alpha$ equipped with an inversion operation, the pointwise inversion of the universal set is the universal set itself, i.e., $(\text{univ} : \text{Set } \alpha)^{-1} = \text{univ}$.

Set.inter_inv theorem

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

Full source

@[to_additive (attr := simp)]
theorem inter_inv : (s ∩ t)⁻¹ = s⁻¹s⁻¹ ∩ t⁻¹ :=
  preimage_inter

Inversion Preserves Set Intersection: $(s \cap t)^{-1} = s^{-1} \cap t^{-1}$

Informal description

For any two sets $s$ and $t$ in a type $\alpha$ equipped with an inversion operation, the pointwise inversion of their intersection equals the intersection of their pointwise inversions. In symbols: $$ (s \cap t)^{-1} = s^{-1} \cap t^{-1} $$

Set.union_inv theorem

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

Full source

@[to_additive (attr := simp)]
theorem union_inv : (s ∪ t)⁻¹ = s⁻¹s⁻¹ ∪ t⁻¹ :=
  preimage_union

Inversion Preserves Set Union: $(s \cup t)^{-1} = s^{-1} \cup t^{-1}$

Informal description

For any two sets $s$ and $t$ in a type $\alpha$ equipped with an inversion operation, the pointwise inversion of their union equals the union of their pointwise inversions. In symbols: $$ (s \cup t)^{-1} = s^{-1} \cup t^{-1} $$

Set.compl_inv theorem

: sᶜ⁻¹ = s⁻¹ᶜ

Full source

@[to_additive (attr := simp)]
theorem compl_inv : sᶜsᶜ⁻¹ = s⁻¹s⁻¹ᶜ :=
  preimage_compl

Inversion of Complement Equals Complement of Inversion for Sets

Informal description

For any set $s$ in a type $\alpha$ equipped with an inversion operation, the pointwise inversion of the complement of $s$ is equal to the complement of the pointwise inversion of $s$. In symbols: $$ (s^c)^{-1} = (s^{-1})^c $$

Set.inv_prod theorem

[Inv β] (s : Set α) (t : Set β) : (s ×ˢ t)⁻¹ = s⁻¹ ×ˢ t⁻¹

Full source

@[to_additive (attr := simp) neg_prod]
lemma inv_prod [Inv β] (s : Set α) (t : Set β) : (s ×ˢ t)⁻¹ = s⁻¹ ×ˢ t⁻¹ := rfl

Inversion of Cartesian Product Equals Product of Inversions

Informal description

For any sets $s \subseteq \alpha$ and $t \subseteq \beta$ where $\alpha$ and $\beta$ are types equipped with inversion operations, the pointwise inversion of the Cartesian product $s \times t$ is equal to the Cartesian product of the pointwise inversions of $s$ and $t$. In symbols: $$ (s \times t)^{-1} = s^{-1} \times t^{-1} $$

Set.inv_mem_inv theorem

: a⁻¹ ∈ s⁻¹ ↔ a ∈ s

Full source

@[to_additive]
theorem inv_mem_inv : a⁻¹a⁻¹ ∈ s⁻¹a⁻¹ ∈ s⁻¹ ↔ a ∈ s := by simp only [mem_inv, inv_inv]

Membership in Pointwise Inverse Set: $a^{-1} \in s^{-1} \leftrightarrow a \in s$

Informal description

For any element $a$ in a type $\alpha$ equipped with an inversion operation and any subset $s$ of $\alpha$, the inverse $a^{-1}$ belongs to the pointwise inverse set $s^{-1}$ if and only if $a$ belongs to $s$. In symbols: $$ a^{-1} \in s^{-1} \leftrightarrow a \in s $$

Set.nonempty_inv theorem

: s⁻¹.Nonempty ↔ s.Nonempty

Full source

@[to_additive (attr := simp)]
theorem nonempty_inv : s⁻¹s⁻¹.Nonempty ↔ s.Nonempty :=
  inv_involutive.surjective.nonempty_preimage

Nonempty Characterization of Pointwise Inverse Sets: $s^{-1} \neq \emptyset \iff s \neq \emptyset$

Informal description

For any set $s$ in a type $\alpha$ equipped with an involutive inversion operation, the pointwise inverse set $s^{-1} = \{x^{-1} \mid x \in s\}$ is nonempty if and only if $s$ is nonempty.

Set.Nonempty.inv theorem

(h : s.Nonempty) : s⁻¹.Nonempty

Full source

@[to_additive]
theorem Nonempty.inv (h : s.Nonempty) : s⁻¹.Nonempty :=
  nonempty_inv.2 h

Nonempty Preservation under Pointwise Inversion

Informal description

For any nonempty set $s$ in a type $\alpha$ equipped with an inversion operation, the pointwise inverse set $s^{-1} = \{x^{-1} \mid x \in s\}$ is also nonempty.

Set.image_inv_eq_inv theorem

: (·⁻¹) '' s = s⁻¹

Full source

@[to_additive (attr := simp)]
theorem image_inv_eq_inv : (·⁻¹) '' s = s⁻¹ :=
  congr_fun (image_eq_preimage_of_inverse inv_involutive.leftInverse inv_involutive.rightInverse) _

Image of Set under Inversion Equals Pointwise Inversion

Informal description

For any set $s$ in a type $\alpha$ equipped with an inversion operation, the image of $s$ under the inversion function is equal to the pointwise inversion of $s$, i.e., $\{x^{-1} \mid x \in s\} = s^{-1}$.

Set.inv_eq_empty theorem

: s⁻¹ = ∅ ↔ s = ∅

Full source

@[to_additive (attr := simp)]
theorem inv_eq_empty : s⁻¹s⁻¹ = ∅ ↔ s = ∅ := by
  rw [← image_inv_eq_inv, image_eq_empty]

Empty Set Characterization via Pointwise Inversion: $s^{-1} = \emptyset \leftrightarrow s = \emptyset$

Informal description

For any set $s$ in a type $\alpha$ equipped with an inversion operation, the pointwise inversion of $s$ is empty if and only if $s$ is empty. In symbols: $$ s^{-1} = \emptyset \leftrightarrow s = \emptyset. $$

Set.involutiveInv instance

: InvolutiveInv (Set α)

Full source

@[to_additive (attr := simp)]
noncomputable instance involutiveInv : InvolutiveInv (Set α) where
  inv := Inv.inv
  inv_inv s := by simp only [← inv_preimage, preimage_preimage, inv_inv, preimage_id']

Pointwise Inversion of Sets Preserves Involutive Property

Informal description

For any type $\alpha$ equipped with an involutive inversion operation, the set of all subsets of $\alpha$ also forms an involutive inversion structure, where the inversion of a set $s$ is defined pointwise as $s^{-1} = \{x^{-1} \mid x \in s\}$.

Set.inv_subset_inv theorem

: s⁻¹ ⊆ t⁻¹ ↔ s ⊆ t

Full source

@[to_additive (attr := simp)]
theorem inv_subset_inv : s⁻¹s⁻¹ ⊆ t⁻¹s⁻¹ ⊆ t⁻¹ ↔ s ⊆ t :=
  (Equiv.inv α).surjective.preimage_subset_preimage_iff

Inversion Preserves Subset Relation: $s^{-1} \subseteq t^{-1} \leftrightarrow s \subseteq t$

Informal description

For any two sets $s$ and $t$ in a type $\alpha$ equipped with an inversion operation, the pointwise inversion of $s$ is contained in the pointwise inversion of $t$ if and only if $s$ is contained in $t$. In symbols: $$ s^{-1} \subseteq t^{-1} \leftrightarrow s \subseteq t. $$

Set.inv_subset theorem

: s⁻¹ ⊆ t ↔ s ⊆ t⁻¹

Full source

@[to_additive]
theorem inv_subset : s⁻¹s⁻¹ ⊆ ts⁻¹ ⊆ t ↔ s ⊆ t⁻¹ := by rw [← inv_subset_inv, inv_inv]

Subset Relation under Pointwise Inversion: $s^{-1} \subseteq t \leftrightarrow s \subseteq t^{-1}$

Informal description

For any two sets $s$ and $t$ in a type $\alpha$ equipped with an inversion operation, the pointwise inversion of $s$ is contained in $t$ if and only if $s$ is contained in the pointwise inversion of $t$. In symbols: $$ s^{-1} \subseteq t \leftrightarrow s \subseteq t^{-1}. $$

Set.inv_singleton theorem

(a : α) : ({ a } : Set α)⁻¹ = {a⁻¹}

Full source

@[to_additive (attr := simp)]
theorem inv_singleton (a : α) : ({a} : Set α)⁻¹ = {a⁻¹} := by
  rw [← image_inv_eq_inv, image_singleton]

Inversion of Singleton Set: $\{a\}^{-1} = \{a^{-1}\}$

Informal description

For any element $a$ in a type $\alpha$ equipped with an inversion operation, the pointwise inversion of the singleton set $\{a\}$ is the singleton set $\{a^{-1}\}$. In symbols: $$ \{a\}^{-1} = \{a^{-1}\}. $$

Set.inv_insert theorem

(a : α) (s : Set α) : (insert a s)⁻¹ = insert a⁻¹ s⁻¹

Full source

@[to_additive (attr := simp)]
theorem inv_insert (a : α) (s : Set α) : (insert a s)⁻¹ = insert a⁻¹ s⁻¹ := by
  rw [insert_eq, union_inv, inv_singleton, insert_eq]

Inversion of Inserted Set: $(\{a\} \cup s)^{-1} = \{a^{-1}\} \cup s^{-1}$

Informal description

For any element $a$ in a type $\alpha$ equipped with an inversion operation and any set $s \subseteq \alpha$, the pointwise inversion of the set $\{a\} \cup s$ is equal to $\{a^{-1}\} \cup s^{-1}$. In symbols: $$ (\{a\} \cup s)^{-1} = \{a^{-1}\} \cup s^{-1}. $$

Set.inv_range theorem

{ι : Sort*} {f : ι → α} : (range f)⁻¹ = range fun i => (f i)⁻¹

Full source

@[to_additive]
theorem inv_range {ι : Sort*} {f : ι → α} : (range f)⁻¹ = range fun i => (f i)⁻¹ := by
  rw [← image_inv_eq_inv]
  exact (range_comp ..).symm

Inversion of Range Equals Range of Inverses

Informal description

For any function $f : \iota \to \alpha$ where $\alpha$ is equipped with an inversion operation, the pointwise inversion of the range of $f$ is equal to the range of the function that applies inversion to each element of $f$. That is, $$(\mathrm{range}\, f)^{-1} = \mathrm{range}\, (f^{-1}) = \{ (f(i))^{-1} \mid i \in \iota \}.$$

Set.image_op_inv theorem

: op '' s⁻¹ = (op '' s)⁻¹

Full source

@[to_additive]
theorem image_op_inv : opop '' s⁻¹ = (op '' s)⁻¹ := by
  simp_rw [← image_inv_eq_inv, Function.Semiconj.set_image op_inv s]

Inversion Commutes with Multiplicative Opposite Image: $\text{op}(s^{-1}) = (\text{op}(s))^{-1}$

Informal description

For any set $s$ in a type $\alpha$ equipped with an inversion operation, the image of the inverted set $s^{-1} = \{x^{-1} \mid x \in s\}$ under the multiplicative opposite embedding $\text{op} : \alpha \to \alpha^\text{op}$ is equal to the inversion of the image of $s$ under $\text{op}$. That is, \[ \text{op}(s^{-1}) = (\text{op}(s))^{-1}. \]

Set.mul definition

: Mul (Set α)

Full source

/-- The pointwise multiplication of sets `s * t` and `t` is defined as `{x * y | x ∈ s, y ∈ t}` in
locale `Pointwise`. -/
@[to_additive
      "The pointwise addition of sets `s + t` is defined as `{x + y | x ∈ s, y ∈ t}` in locale
      `Pointwise`."]
protected def mul : Mul (Set α) :=
  ⟨image2 (· * ·)⟩

Pointwise multiplication of sets

Informal description

The pointwise multiplication of sets $s$ and $t$ in a type $\alpha$ equipped with a multiplication operation is defined as the set $\{x \cdot y \mid x \in s, y \in t\}$ of all possible products of elements from $s$ and $t$.

Set.image2_mul theorem

: image2 (· * ·) s t = s * t

Full source

@[to_additive (attr := simp)]
theorem image2_mul : image2 (· * ·) s t = s * t :=
  rfl

Image of Multiplication Function Equals Pointwise Product of Sets

Informal description

For any sets $s$ and $t$ in a type $\alpha$ equipped with a multiplication operation, the image of the multiplication function under $s$ and $t$ is equal to their pointwise product, i.e., \[ \text{image2}(\cdot, s, t) = s \cdot t. \] Here, $\text{image2}(\cdot, s, t)$ denotes the set $\{x \cdot y \mid x \in s, y \in t\}$ and $s \cdot t$ is the pointwise product of $s$ and $t$.

Set.mem_mul theorem

: a ∈ s * t ↔ ∃ x ∈ s, ∃ y ∈ t, x * y = a

Full source

@[to_additive]
theorem mem_mul : a ∈ s * ta ∈ s * t ↔ ∃ x ∈ s, ∃ y ∈ t, x * y = a :=
  Iff.rfl

Membership in Pointwise Product of Sets

Informal description

An element $a$ belongs to the pointwise product of sets $s$ and $t$ if and only if there exist elements $x \in s$ and $y \in t$ such that $x \cdot y = a$. In symbols: $$ a \in s \cdot t \iff \exists x \in s, \exists y \in t, x \cdot y = a $$

Set.mul_mem_mul theorem

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

Full source

@[to_additive]
theorem mul_mem_mul : a ∈ s → b ∈ t → a * b ∈ s * t :=
  mem_image2_of_mem

Membership in Pointwise Product of Sets

Informal description

For any elements $a \in s$ and $b \in t$, the product $a \cdot b$ belongs to the pointwise product set $s \cdot t$.

Set.image_mul_prod theorem

: (fun x : α × α => x.fst * x.snd) '' s ×ˢ t = s * t

Full source

@[to_additive add_image_prod]
theorem image_mul_prod : (fun x : α × α => x.fst * x.snd) '' s ×ˢ t = s * t :=
  image_prod _

Equality of Cartesian Product Image and Pointwise Product Set

Informal description

For any sets $s, t \subseteq \alpha$ in a type $\alpha$ equipped with a multiplication operation, the image of the Cartesian product $s \times t$ under the multiplication map $(x,y) \mapsto x \cdot y$ is equal to the pointwise product set $s \cdot t$. In symbols: $$ \{(x \cdot y) \mid (x,y) \in s \times t\} = s \cdot t. $$

Set.empty_mul theorem

: ∅ * s = ∅

Full source

@[to_additive (attr := simp)]
theorem empty_mul : ∅ * s = ∅ :=
  image2_empty_left

Empty Set Multiplication Property: $\emptyset \cdot s = \emptyset$

Informal description

For any set $s$ in a type $\alpha$ equipped with a multiplication operation, the product of the empty set and $s$ is the empty set, i.e., $\emptyset \cdot s = \emptyset$.

Set.mul_empty theorem

: s * ∅ = ∅

Full source

@[to_additive (attr := simp)]
theorem mul_empty : s * ∅ = ∅ :=
  image2_empty_right

Multiplication of a Set with the Empty Set Yields the Empty Set

Informal description

For any set $s$ in a type $\alpha$ equipped with a multiplication operation, the pointwise product of $s$ with the empty set is the empty set, i.e., $s \cdot \emptyset = \emptyset$.

Set.mul_eq_empty theorem

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

Full source

@[to_additive (attr := simp)]
theorem mul_eq_empty : s * t = ∅ ↔ s = ∅ ∨ t = ∅ :=
  image2_eq_empty_iff

Product of Sets is Empty iff Either Set is Empty

Informal description

For any sets $s$ and $t$ in a type $\alpha$ equipped with a multiplication operation, the pointwise product set $s \cdot t = \{x \cdot y \mid x \in s, y \in t\}$ is empty if and only if either $s$ is empty or $t$ is empty. That is, $s \cdot t = \emptyset \leftrightarrow s = \emptyset \lor t = \emptyset$.

Set.mul_nonempty theorem

: (s * t).Nonempty ↔ s.Nonempty ∧ t.Nonempty

Full source

@[to_additive (attr := simp)]
theorem mul_nonempty : (s * t).Nonempty ↔ s.Nonempty ∧ t.Nonempty :=
  image2_nonempty_iff

Nonempty Product of Sets iff Both Sets Nonempty

Informal description

For any sets $s$ and $t$ in a type $\alpha$ equipped with a multiplication operation, the pointwise product set $s \cdot t = \{x \cdot y \mid x \in s, y \in t\}$ is nonempty if and only if both $s$ and $t$ are nonempty.

Set.Nonempty.mul theorem

: s.Nonempty → t.Nonempty → (s * t).Nonempty

Full source

@[to_additive]
theorem Nonempty.mul : s.Nonempty → t.Nonempty → (s * t).Nonempty :=
  Nonempty.image2

Nonempty Product of Nonempty Sets

Informal description

For any nonempty sets $s$ and $t$ in a type $\alpha$ equipped with a multiplication operation, the pointwise product set $s \cdot t = \{x \cdot y \mid x \in s, y \in t\}$ is nonempty.

Set.Nonempty.of_mul_left theorem

: (s * t).Nonempty → s.Nonempty

Full source

@[to_additive]
theorem Nonempty.of_mul_left : (s * t).Nonempty → s.Nonempty :=
  Nonempty.of_image2_left

Nonemptiness of Left Factor in Nonempty Product Set

Informal description

If the pointwise product set $s \cdot t = \{x \cdot y \mid x \in s, y \in t\}$ is nonempty, then the set $s$ is nonempty.

Set.Nonempty.of_mul_right theorem

: (s * t).Nonempty → t.Nonempty

Full source

@[to_additive]
theorem Nonempty.of_mul_right : (s * t).Nonempty → t.Nonempty :=
  Nonempty.of_image2_right

Nonemptiness of Right Factor in Nonempty Product Set

Informal description

If the pointwise product set $s \cdot t = \{x \cdot y \mid x \in s, y \in t\}$ is nonempty, then the set $t$ is nonempty.

Set.mul_singleton theorem

: s * { b } = (· * b) '' s

Full source

@[to_additive (attr := simp)]
theorem mul_singleton : s * {b} = (· * b) '' s :=
  image2_singleton_right

Pointwise Multiplication of Set with Singleton: $s \cdot \{b\} = \{x \cdot b \mid x \in s\}$

Informal description

For any set $s$ in a type $\alpha$ equipped with a multiplication operation and any element $b \in \alpha$, the pointwise product of $s$ with the singleton set $\{b\}$ is equal to the image of $s$ under the function $\lambda x, x \cdot b$. In other words, $s \cdot \{b\} = \{x \cdot b \mid x \in s\}$.

Set.singleton_mul theorem

: { a } * t = (a * ·) '' t

Full source

@[to_additive (attr := simp)]
theorem singleton_mul : {a} * t = (a * ·) '' t :=
  image2_singleton_left

Pointwise multiplication of a singleton set: $\{a\} \cdot t = \{a \cdot x \mid x \in t\}$

Informal description

For any element $a$ in a type $\alpha$ equipped with a multiplication operation, and any subset $t \subseteq \alpha$, the pointwise product of the singleton set $\{a\}$ with $t$ is equal to the image of $t$ under the function $x \mapsto a \cdot x$. That is, $\{a\} \cdot t = \{a \cdot x \mid x \in t\}$.

Set.singleton_mul_singleton theorem

: ({ a } : Set α) * { b } = {a * b}

Full source

@[to_additive]
theorem singleton_mul_singleton : ({a} : Set α) * {b} = {a * b} :=
  image2_singleton

Pointwise Product of Singleton Sets: $\{a\} \cdot \{b\} = \{a \cdot b\}$

Informal description

For any elements $a$ and $b$ in a type $\alpha$ equipped with a multiplication operation, the pointwise product of the singleton sets $\{a\}$ and $\{b\}$ is the singleton set $\{a \cdot b\}$. In other words, $\{a\} \cdot \{b\} = \{a \cdot b\}$.

Set.mul_subset_mul theorem

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

Full source

@[to_additive (attr := mono, gcongr)]
theorem mul_subset_mul : s₁ ⊆ t₁ → s₂ ⊆ t₂ → s₁ * s₂ ⊆ t₁ * t₂ :=
  image2_subset

Monotonicity of Pointwise Set Multiplication under Subset Inclusion

Informal description

For any subsets $s_1, t_1 \subseteq \alpha$ and $s_2, t_2 \subseteq \alpha$ in a type $\alpha$ equipped with a multiplication operation, if $s_1 \subseteq t_1$ and $s_2 \subseteq t_2$, then the pointwise product $s_1 \cdot s_2$ is a subset of $t_1 \cdot t_2$.

Set.mul_subset_mul_left theorem

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

Full source

@[to_additive (attr := gcongr)]
theorem mul_subset_mul_left : t₁ ⊆ t₂ → s * t₁ ⊆ s * t₂ :=
  image2_subset_left

Left Monotonicity of Pointwise Set Multiplication: $t_1 \subseteq t_2 \Rightarrow s \cdot t_1 \subseteq s \cdot t_2$

Informal description

For any subsets $s, t_1, t_2$ of a type $\alpha$ equipped with a multiplication operation, if $t_1 \subseteq t_2$, then the pointwise product $s \cdot t_1$ is a subset of $s \cdot t_2$.

Set.mul_subset_mul_right theorem

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

Full source

@[to_additive (attr := gcongr)]
theorem mul_subset_mul_right : s₁ ⊆ s₂ → s₁ * t ⊆ s₂ * t :=
  image2_subset_right

Right Monotonicity of Pointwise Set Multiplication

Informal description

For any subsets $s_1, s_2, t$ of a type $\alpha$ equipped with a multiplication operation, if $s_1 \subseteq s_2$, then the pointwise product $s_1 \cdot t$ is a subset of $s_2 \cdot t$.

Set.instMulLeftMono instance

: MulLeftMono (Set α)

Full source

@[to_additive] instance : MulLeftMono (Set α) where elim _s _t₁ _t₂ := mul_subset_mul_left

Monotonicity of Left Multiplication on Subsets

Informal description

For any type $\alpha$ with a multiplication operation, the collection of subsets of $\alpha$ satisfies the property that left multiplication by any fixed subset is monotone with respect to subset inclusion. That is, for any subsets $s, t_1, t_2 \subseteq \alpha$, if $t_1 \subseteq t_2$, then $s \cdot t_1 \subseteq s \cdot t_2$.

Set.instMulRightMono instance

: MulRightMono (Set α)

Full source

@[to_additive] instance : MulRightMono (Set α) where elim _t _s₁ _s₂ := mul_subset_mul_right

Right Monotonicity of Pointwise Set Multiplication

Informal description

For any type $\alpha$ equipped with a multiplication operation, the pointwise multiplication of sets in $\alpha$ is right-monotone. That is, for any sets $s, t_1, t_2 \subseteq \alpha$, if $t_1 \subseteq t_2$, then $s \cdot t_1 \subseteq s \cdot t_2$.

Set.mul_subset_iff theorem

: s * t ⊆ u ↔ ∀ x ∈ s, ∀ y ∈ t, x * y ∈ u

Full source

@[to_additive]
theorem mul_subset_iff : s * t ⊆ us * t ⊆ u ↔ ∀ x ∈ s, ∀ y ∈ t, x * y ∈ u :=
  image2_subset_iff

Subset condition for pointwise multiplication of sets

Informal description

For sets $s$, $t$, and $u$ in a type $\alpha$ equipped with a multiplication operation, the pointwise product set $s \cdot t$ is a subset of $u$ if and only if for every $x \in s$ and $y \in t$, the product $x \cdot y$ belongs to $u$. In other words: \[ s \cdot t \subseteq u \leftrightarrow \forall x \in s, \forall y \in t, x \cdot y \in u. \]

Set.union_mul theorem

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

Full source

@[to_additive]
theorem union_mul : (s₁ ∪ s₂) * t = s₁ * t ∪ s₂ * t :=
  image2_union_left

Distributivity of Pointwise Multiplication over Union in First Argument: $(s_1 \cup s_2) \cdot t = s_1 \cdot t \cup s_2 \cdot t$

Informal description

For any sets $s_1, s_2, t$ in a type $\alpha$ equipped with a multiplication operation, the pointwise product of the union $s_1 \cup s_2$ with $t$ equals the union of the pointwise products $s_1 \cdot t$ and $s_2 \cdot t$. That is: \[ (s_1 \cup s_2) \cdot t = s_1 \cdot t \cup s_2 \cdot t. \]

Set.mul_union theorem

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

Full source

@[to_additive]
theorem mul_union : s * (t₁ ∪ t₂) = s * t₁ ∪ s * t₂ :=
  image2_union_right

Distributivity of Pointwise Multiplication over Union in Second Argument: $s \cdot (t_1 \cup t_2) = s \cdot t_1 \cup s \cdot t_2$

Informal description

For any sets $s$, $t_1$, and $t_2$ in a type $\alpha$ equipped with a multiplication operation, the pointwise product of $s$ with the union $t_1 \cup t_2$ equals the union of the pointwise products $s \cdot t_1$ and $s \cdot t_2$. That is: \[ s \cdot (t_1 \cup t_2) = s \cdot t_1 \cup s \cdot t_2. \]

Set.inter_mul_subset theorem

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

Full source

@[to_additive]
theorem inter_mul_subset : s₁ ∩ s₂s₁ ∩ s₂ * t ⊆ s₁ * t ∩ (s₂ * t) :=
  image2_inter_subset_left

Subset Property of Pointwise Multiplication over Intersection in First Argument

Informal description

For any sets $s_1, s_2, t$ in a type $\alpha$ equipped with a multiplication operation, the pointwise product of the intersection $s_1 \cap s_2$ with $t$ is a subset of the intersection of the pointwise products $s_1 \cdot t$ and $s_2 \cdot t$. That is: \[ (s_1 \cap s_2) \cdot t \subseteq s_1 \cdot t \cap s_2 \cdot t. \]

Set.mul_inter_subset theorem

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

Full source

@[to_additive]
theorem mul_inter_subset : s * (t₁ ∩ t₂) ⊆ s * t₁ ∩ (s * t₂) :=
  image2_inter_subset_right

Subset Property of Pointwise Multiplication over Intersection: $s \cdot (t_1 \cap t_2) \subseteq s \cdot t_1 \cap s \cdot t_2$

Informal description

For any sets $s$, $t_1$, and $t_2$ in a type $\alpha$ equipped with a multiplication operation, the pointwise product of $s$ with the intersection $t_1 \cap t_2$ is a subset of the intersection of the pointwise products $s \cdot t_1$ and $s \cdot t_2$. That is: \[ s \cdot (t_1 \cap t_2) \subseteq s \cdot t_1 \cap s \cdot t_2. \]

Set.inter_mul_union_subset_union theorem

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

Full source

@[to_additive]
theorem inter_mul_union_subset_union : s₁ ∩ s₂s₁ ∩ s₂ * (t₁ ∪ t₂) ⊆ s₁ * t₁ ∪ s₂ * t₂ :=
  image2_inter_union_subset_union

Subset Property for Pointwise Multiplication of Intersection and Union

Informal description

For any sets $s_1, s_2, t_1, t_2$ in a type $\alpha$ equipped with a multiplication operation, the pointwise product of the intersection $s_1 \cap s_2$ with the union $t_1 \cup t_2$ is contained in the union of the pointwise products $s_1 \cdot t_1$ and $s_2 \cdot t_2$. In other words: \[ (s_1 \cap s_2) \cdot (t_1 \cup t_2) \subseteq s_1 \cdot t_1 \cup s_2 \cdot t_2 \]

Set.union_mul_inter_subset_union theorem

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

Full source

@[to_additive]
theorem union_mul_inter_subset_union : (s₁ ∪ s₂) * (t₁ ∩ t₂) ⊆ s₁ * t₁ ∪ s₂ * t₂ :=
  image2_union_inter_subset_union

Union-Intersection Subset Property for Pointwise Multiplication

Informal description

For any sets $s_1, s_2, t_1, t_2$ in a type $\alpha$ equipped with a multiplication operation, the pointwise product of the union $s_1 \cup s_2$ with the intersection $t_1 \cap t_2$ is contained in the union of the products $s_1 * t_1$ and $s_2 * t_2$. That is, $$(s_1 \cup s_2) \cdot (t_1 \cap t_2) \subseteq (s_1 \cdot t_1) \cup (s_2 \cdot t_2).$$

Set.singletonMulHom definition

: α →ₙ* Set α

Full source

/-- The singleton operation as a `MulHom`. -/
@[to_additive "The singleton operation as an `AddHom`."]
noncomputable def singletonMulHom : α →ₙ* Set α where
  toFun := singleton
  map_mul' _ _ := singleton_mul_singleton.symm

Singleton multiplicative homomorphism

Informal description

The function that maps an element $a$ of a type $\alpha$ with multiplication to the singleton set $\{a\}$ is a multiplicative homomorphism, i.e., it satisfies $\{a \cdot b\} = \{a\} \cdot \{b\}$ for all $a, b \in \alpha$.

Set.coe_singletonMulHom theorem

: (singletonMulHom : α → Set α) = singleton

Full source

@[to_additive (attr := simp)]
theorem coe_singletonMulHom : (singletonMulHom : α → Set α) = singleton :=
  rfl

Equality of Singleton Multiplicative Homomorphism and Singleton Function

Informal description

The function `singletonMulHom` from a type $\alpha$ to the type of sets over $\alpha$ is equal to the singleton set function, i.e., for any $a \in \alpha$, `singletonMulHom a = {a}`.

Set.singletonMulHom_apply theorem

(a : α) : singletonMulHom a = { a }

Full source

@[to_additive (attr := simp)]
theorem singletonMulHom_apply (a : α) : singletonMulHom a = {a} :=
  rfl

Singleton multiplicative homomorphism maps element to singleton set: $\text{singletonMulHom}(a) = \{a\}$

Informal description

For any element $a$ of a type $\alpha$, the multiplicative homomorphism `singletonMulHom` maps $a$ to the singleton set $\{a\}$, i.e., $\text{singletonMulHom}(a) = \{a\}$.

Set.image_op_mul theorem

: op '' (s * t) = op '' t * op '' s

Full source

@[to_additive (attr := simp)]
theorem image_op_mul : opop '' (s * t) = opop '' t * opop '' s :=
  image_image2_antidistrib op_mul

Image of Pointwise Product under Multiplicative Opposite: $\text{op}(s \cdot t) = \text{op}(t) \cdot \text{op}(s)$

Informal description

For any subsets $s$ and $t$ of a type $\alpha$ equipped with a multiplication operation, the image of the pointwise product $s \cdot t$ under the canonical embedding $\text{op} : \alpha \to \alpha^\text{op}$ equals the pointwise product of the images $\text{op}(t) \cdot \text{op}(s)$ in the multiplicative opposite $\alpha^\text{op}$. In other words: \[ \text{op}(s \cdot t) = \text{op}(t) \cdot \text{op}(s) \]

Set.prod_mul_prod_comm theorem

 [Mul β] (s₁ s₂ : Set α) (t₁ t₂ : Set β) : (s₁ ×ˢ t₁) * (s₂ ×ˢ t₂) = (s₁ * s₂) ×ˢ (t₁ * t₂)

Full source

@[to_additive (attr := simp) prod_add_prod_comm]
lemma prod_mul_prod_comm [Mul β] (s₁ s₂: Set α) (t₁ t₂ : Set β) :
   (s₁ ×ˢ t₁) * (s₂ ×ˢ t₂) = (s₁ * s₂) ×ˢ (t₁ * t₂) := by ext; simp [mem_mul]; aesop

Commutativity of Cartesian Product with Pointwise Multiplication: $(s_1 \times t_1) \cdot (s_2 \times t_2) = (s_1 \cdot s_2) \times (t_1 \cdot t_2)$

Informal description

Let $\alpha$ and $\beta$ be types equipped with multiplication operations. For any subsets $s_1, s_2 \subseteq \alpha$ and $t_1, t_2 \subseteq \beta$, the pointwise product of the Cartesian products $s_1 \times t_1$ and $s_2 \times t_2$ equals the Cartesian product of the pointwise products $(s_1 \cdot s_2) \times (t_1 \cdot t_2)$. In other words: $$(s_1 \times t_1) \cdot (s_2 \times t_2) = (s_1 \cdot s_2) \times (t_1 \cdot t_2)$$ where $\cdot$ denotes pointwise multiplication and $\times$ denotes Cartesian product.

Set.div definition

: Div (Set α)

Full source

/-- The pointwise division of sets `s / t` is defined as `{x / y | x ∈ s, y ∈ t}` in locale
`Pointwise`. -/
@[to_additive
      "The pointwise subtraction of sets `s - t` is defined as `{x - y | x ∈ s, y ∈ t}` in locale
      `Pointwise`."]
protected def div : Div (Set α) :=
  ⟨image2 (· / ·)⟩

Pointwise division of sets

Informal description

The pointwise division of sets $s$ and $t$ in a type $\alpha$ with a division operation is defined as the set $\{x / y \mid x \in s, y \in t\}$.

Set.image2_div theorem

: image2 (· / ·) s t = s / t

Full source

@[to_additive (attr := simp)]
theorem image2_div : image2 (· / ·) s t = s / t :=
  rfl

Image of Division Function Equals Pointwise Division of Sets

Informal description

For any sets $s$ and $t$ in a type $\alpha$ equipped with a division operation, the image of the division function applied to $s$ and $t$ is equal to the pointwise division of $s$ and $t$, i.e., \[ \text{image2}(\cdot / \cdot, s, t) = s / t. \]

Set.mem_div theorem

: a ∈ s / t ↔ ∃ x ∈ s, ∃ y ∈ t, x / y = a

Full source

@[to_additive]
theorem mem_div : a ∈ s / ta ∈ s / t ↔ ∃ x ∈ s, ∃ y ∈ t, x / y = a :=
  Iff.rfl

Membership in Pointwise Division of Sets

Informal description

An element $a$ belongs to the pointwise division of sets $s$ and $t$ if and only if there exist elements $x \in s$ and $y \in t$ such that $x / y = a$. In other words: \[ a \in s / t \iff \exists x \in s, \exists y \in t, x / y = a \]

Set.div_mem_div theorem

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

Full source

@[to_additive]
theorem div_mem_div : a ∈ s → b ∈ t → a / b ∈ s / t :=
  mem_image2_of_mem

Closure of Pointwise Division under Division Operation

Informal description

For any elements $a \in s$ and $b \in t$ in a type $\alpha$ with a division operation, the quotient $a / b$ belongs to the pointwise division set $s / t$.

Set.image_div_prod theorem

: (fun x : α × α => x.fst / x.snd) '' s ×ˢ t = s / t

Full source

@[to_additive sub_image_prod]
theorem image_div_prod : (fun x : α × α => x.fst / x.snd) '' s ×ˢ t = s / t :=
  image_prod _

Equality of Cartesian Product Image and Pointwise Division

Informal description

For any sets $s, t \subseteq \alpha$ in a type $\alpha$ with a division operation, the image of the Cartesian product $s \times t$ under the division function $(x,y) \mapsto x/y$ is equal to the pointwise division set $s / t$. In other words: $$ \{(x/y) \mid (x,y) \in s \times t\} = \{x/y \mid x \in s, y \in t\} $$

Set.empty_div theorem

: ∅ / s = ∅

Full source

@[to_additive (attr := simp)]
theorem empty_div : ∅ / s = ∅ :=
  image2_empty_left

Empty Set Division Property: $\emptyset / s = \emptyset$

Informal description

For any set $s$ in a type $\alpha$ equipped with a division operation, the pointwise division of the empty set by $s$ is the empty set, i.e., $\emptyset / s = \emptyset$.

Set.div_empty theorem

: s / ∅ = ∅

Full source

@[to_additive (attr := simp)]
theorem div_empty : s / ∅ = ∅ :=
  image2_empty_right

Pointwise Division by Empty Set Yields Empty Set

Informal description

For any set $s$ in a type $\alpha$ with a division operation, the pointwise division of $s$ by the empty set is the empty set, i.e., $s / \emptyset = \emptyset$.

Set.div_eq_empty theorem

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

Full source

@[to_additive (attr := simp)]
theorem div_eq_empty : s / t = ∅ ↔ s = ∅ ∨ t = ∅ :=
  image2_eq_empty_iff

Empty Criterion for Pointwise Division of Sets: $s / t = \emptyset \leftrightarrow s = \emptyset \lor t = \emptyset$

Informal description

For any sets $s$ and $t$ in a type $\alpha$ with a division operation, the pointwise division set $s / t = \{x / y \mid x \in s, y \in t\}$ is empty if and only if either $s$ is empty or $t$ is empty. That is, $s / t = \emptyset \leftrightarrow s = \emptyset \lor t = \emptyset$.

Set.div_nonempty theorem

: (s / t).Nonempty ↔ s.Nonempty ∧ t.Nonempty

Full source

@[to_additive (attr := simp)]
theorem div_nonempty : (s / t).Nonempty ↔ s.Nonempty ∧ t.Nonempty :=
  image2_nonempty_iff

Nonempty Criterion for Pointwise Division of Sets

Informal description

For any sets $s$ and $t$ in a type $\alpha$ equipped with a division operation, the pointwise division set $s / t = \{x / y \mid x \in s, y \in t\}$ is nonempty if and only if both $s$ and $t$ are nonempty.

Set.Nonempty.div theorem

: s.Nonempty → t.Nonempty → (s / t).Nonempty

Full source

@[to_additive]
theorem Nonempty.div : s.Nonempty → t.Nonempty → (s / t).Nonempty :=
  Nonempty.image2

Nonempty Pointwise Division of Nonempty Sets

Informal description

For any nonempty sets $s$ and $t$ in a type $\alpha$ equipped with a division operation, the pointwise division set $s / t = \{x / y \mid x \in s, y \in t\}$ is nonempty.

Set.Nonempty.of_div_left theorem

: (s / t).Nonempty → s.Nonempty

Full source

@[to_additive]
theorem Nonempty.of_div_left : (s / t).Nonempty → s.Nonempty :=
  Nonempty.of_image2_left

Nonemptiness of Left Set in Pointwise Division

Informal description

If the pointwise division set $s / t = \{x / y \mid x \in s, y \in t\}$ is nonempty, then the set $s$ is nonempty.

Set.Nonempty.of_div_right theorem

: (s / t).Nonempty → t.Nonempty

Full source

@[to_additive]
theorem Nonempty.of_div_right : (s / t).Nonempty → t.Nonempty :=
  Nonempty.of_image2_right

Nonemptiness of Divisor Set in Pointwise Division

Informal description

If the pointwise division set $s / t = \{x / y \mid x \in s, y \in t\}$ is nonempty, then the set $t$ is nonempty.

Set.div_singleton theorem

: s / { b } = (· / b) '' s

Full source

@[to_additive (attr := simp)]
theorem div_singleton : s / {b} = (· / b) '' s :=
  image2_singleton_right

Pointwise Division by Singleton: $s / \{b\} = \{x / b \mid x \in s\}$

Informal description

For any set $s$ in a type $\alpha$ with a division operation and any element $b \in \alpha$, the pointwise division of $s$ by the singleton set $\{b\}$ is equal to the image of $s$ under the function $\lambda x, x / b$. In other words, $s / \{b\} = \{x / b \mid x \in s\}$.

Set.singleton_div theorem

: { a } / t = (· / ·) a '' t

Full source

@[to_additive (attr := simp)]
theorem singleton_div : {a} / t = (· / ·) a '' t :=
  image2_singleton_left

Pointwise Division of Singleton Set: $\{a\} / t = \{a / b \mid b \in t\}$

Informal description

For any element $a$ in a type $\alpha$ with a division operation and any subset $t \subseteq \alpha$, the pointwise division of the singleton set $\{a\}$ by $t$ is equal to the image of $t$ under the function $\lambda b, a / b$. That is, $\{a\} / t = \{a / b \mid b \in t\}$.

Set.singleton_div_singleton theorem

: ({ a } : Set α) / { b } = {a / b}

Full source

@[to_additive]
theorem singleton_div_singleton : ({a} : Set α) / {b} = {a / b} :=
  image2_singleton

Pointwise Division of Singleton Sets: $\{a\} / \{b\} = \{a / b\}$

Informal description

For any elements $a$ and $b$ in a type $\alpha$ equipped with a division operation, the pointwise division of the singleton set $\{a\}$ by the singleton set $\{b\}$ is the singleton set $\{a / b\}$. In other words, $\{a\} / \{b\} = \{a / b\}$.

Set.div_subset_div theorem

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

Full source

@[to_additive (attr := mono, gcongr)]
theorem div_subset_div : s₁ ⊆ t₁ → s₂ ⊆ t₂ → s₁ / s₂ ⊆ t₁ / t₂ :=
  image2_subset

Monotonicity of Pointwise Division with Respect to Subset Inclusion

Informal description

For any subsets $s_1, t_1, s_2, t_2$ of a type $\alpha$ with a division operation, if $s_1 \subseteq t_1$ and $s_2 \subseteq t_2$, then the pointwise division set $s_1 / s_2$ is a subset of $t_1 / t_2$. Here $s_1 / s_2$ denotes the set $\{x / y \mid x \in s_1, y \in s_2\}$.

Set.div_subset_div_left theorem

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

Full source

@[to_additive (attr := gcongr)]
theorem div_subset_div_left : t₁ ⊆ t₂ → s / t₁ ⊆ s / t₂ :=
  image2_subset_left

Left Monotonicity of Pointwise Division with Respect to Right Subset Inclusion

Informal description

For any subsets $t_1, t_2$ of a type $\alpha$ with a division operation, if $t_1 \subseteq t_2$, then for any subset $s \subseteq \alpha$, the pointwise division set $s / t_1$ is a subset of $s / t_2$. Here $s / t_i$ denotes the set $\{x / y \mid x \in s, y \in t_i\}$.

Set.div_subset_div_right theorem

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

Full source

@[to_additive (attr := gcongr)]
theorem div_subset_div_right : s₁ ⊆ s₂ → s₁ / t ⊆ s₂ / t :=
  image2_subset_right

Right Monotonicity of Pointwise Division with Respect to Subset Inclusion

Informal description

For any sets $s_1, s_2, t$ in a type $\alpha$ equipped with a division operation, if $s_1 \subseteq s_2$, then the pointwise division set $s_1 / t$ is a subset of $s_2 / t$. Here $s_1 / t$ denotes the set $\{x / y \mid x \in s_1, y \in t\}$.

Set.div_subset_iff theorem

: s / t ⊆ u ↔ ∀ x ∈ s, ∀ y ∈ t, x / y ∈ u

Full source

@[to_additive]
theorem div_subset_iff : s / t ⊆ us / t ⊆ u ↔ ∀ x ∈ s, ∀ y ∈ t, x / y ∈ u :=
  image2_subset_iff

Subset condition for pointwise division of sets

Informal description

For sets $s$, $t$, and $u$ in a type $\alpha$ equipped with a division operation, the pointwise division set $s / t$ is a subset of $u$ if and only if for every $x \in s$ and $y \in t$, the division $x / y$ belongs to $u$. In other words: \[ s / t \subseteq u \leftrightarrow \forall x \in s, \forall y \in t, x / y \in u. \]

Set.union_div theorem

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

Full source

@[to_additive]
theorem union_div : (s₁ ∪ s₂) / t = s₁ / t ∪ s₂ / t :=
  image2_union_left

Distributivity of Pointwise Division over Union: $(s_1 \cup s_2)/t = s_1/t \cup s_2/t$

Informal description

For any sets $s_1, s_2, t$ in a type $\alpha$ equipped with a division operation, the pointwise division of the union $s_1 \cup s_2$ by $t$ equals the union of the pointwise divisions of $s_1$ by $t$ and $s_2$ by $t$. That is, \[ (s_1 \cup s_2) / t = (s_1 / t) \cup (s_2 / t). \]

Set.div_union theorem

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

Full source

@[to_additive]
theorem div_union : s / (t₁ ∪ t₂) = s / t₁ ∪ s / t₂ :=
  image2_union_right

Distributivity of Pointwise Division over Union: $s / (t_1 \cup t_2) = s / t_1 \cup s / t_2$

Informal description

For any sets $s$, $t_1$, and $t_2$ in a type $\alpha$ equipped with a division operation, the pointwise division of $s$ by the union $t_1 \cup t_2$ equals the union of the pointwise divisions of $s$ by $t_1$ and $s$ by $t_2$. That is, \[ s / (t_1 \cup t_2) = (s / t_1) \cup (s / t_2). \]

Set.inter_div_subset theorem

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

Full source

@[to_additive]
theorem inter_div_subset : s₁ ∩ s₂s₁ ∩ s₂ / t ⊆ s₁ / t ∩ (s₂ / t) :=
  image2_inter_subset_left

Subset Property of Pointwise Division over Intersection

Informal description

For any sets $s_1, s_2, t$ in a type $\alpha$ equipped with a division operation, the pointwise division of the intersection $s_1 \cap s_2$ by $t$ is a subset of the intersection of the pointwise divisions of $s_1$ by $t$ and $s_2$ by $t$. That is, \[ (s_1 \cap s_2) / t \subseteq (s_1 / t) \cap (s_2 / t). \]

Set.div_inter_subset theorem

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

Full source

@[to_additive]
theorem div_inter_subset : s / (t₁ ∩ t₂) ⊆ s / t₁ ∩ (s / t₂) :=
  image2_inter_subset_right

Subset Property of Pointwise Division over Intersection: $s / (t_1 \cap t_2) \subseteq (s / t_1) \cap (s / t_2)$

Informal description

For any sets $s$, $t_1$, and $t_2$ in a type $\alpha$ equipped with a division operation, the pointwise division of $s$ by the intersection $t_1 \cap t_2$ is a subset of the intersection of the pointwise divisions of $s$ by $t_1$ and $s$ by $t_2$. That is, \[ s / (t_1 \cap t_2) \subseteq (s / t_1) \cap (s / t_2). \]

Set.inter_div_union_subset_union theorem

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

Full source

@[to_additive]
theorem inter_div_union_subset_union : s₁ ∩ s₂s₁ ∩ s₂ / (t₁ ∪ t₂) ⊆ s₁ / t₁ ∪ s₂ / t₂ :=
  image2_inter_union_subset_union

Subset relation for pointwise division of intersection over union

Informal description

For any sets $s_1, s_2, t_1, t_2$ in a type $\alpha$ with a division operation, the following subset relation holds: \[ (s_1 \cap s_2) / (t_1 \cup t_2) \subseteq (s_1 / t_1) \cup (s_2 / t_2), \] where $s / t$ denotes the pointwise division $\{x / y \mid x \in s, y \in t\}$.

Set.union_div_inter_subset_union theorem

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

Full source

@[to_additive]
theorem union_div_inter_subset_union : (s₁ ∪ s₂) / (t₁ ∩ t₂) ⊆ s₁ / t₁ ∪ s₂ / t₂ :=
  image2_union_inter_subset_union

Union Divided by Intersection Subset of Divided Unions: $(s_1 \cup s_2)/(t_1 \cap t_2) \subseteq (s_1/t_1) \cup (s_2/t_2)$

Informal description

For any sets $s_1, s_2, t_1, t_2$ in a type $\alpha$ equipped with a division operation, the pointwise division of the union $s_1 \cup s_2$ by the intersection $t_1 \cap t_2$ is a subset of the union of the pointwise divisions $s_1 / t_1$ and $s_2 / t_2$. That is, \[ (s_1 \cup s_2) / (t_1 \cap t_2) \subseteq (s_1 / t_1) \cup (s_2 / t_2). \]

Set.NSMul definition

[Zero α] [Add α] : SMul ℕ (Set α)

Full source

/-- Repeated pointwise addition (not the same as pointwise repeated addition!) of a `Set`. See
note [pointwise nat action]. -/
protected def NSMul [Zero α] [Add α] : SMul ℕ (Set α) :=
  ⟨nsmulRec⟩

Natural number scalar multiplication on sets via repeated addition

Informal description

The definition of scalar multiplication of a natural number $ n $ on a set $ s $ in an additive monoid, given by repeated pointwise addition of the set to itself $ n $ times. That is, $ n \cdot s = \{ x_1 + \dots + x_n \mid x_i \in s \} $.

Set.NPow definition

[One α] [Mul α] : Pow (Set α) ℕ

Full source

/-- Repeated pointwise multiplication (not the same as pointwise repeated multiplication!) of a
`Set`. See note [pointwise nat action]. -/
@[to_additive existing]
protected def NPow [One α] [Mul α] : Pow (Set α) ℕ :=
  ⟨fun s n => npowRec n s⟩

Natural number power operation on sets (repeated pointwise multiplication)

Informal description

For a type $\alpha$ equipped with a multiplication operation and a multiplicative identity, the natural number power operation on sets is defined as the repeated pointwise multiplication of a set $s$ with itself $n$ times, where $n$ is a natural number. Specifically: - For $n = 0$, it returns the singleton set $\{1\}$. - For $n > 0$, it recursively computes the pointwise product $s \cdot \text{npowRec} (n-1) s$. Note that this differs from pointwise exponentiation (where each element is raised to the power $n$).

Set.ZSMul definition

[Zero α] [Add α] [Neg α] : SMul ℤ (Set α)

Full source

/-- Repeated pointwise addition/subtraction (not the same as pointwise repeated
addition/subtraction!) of a `Set`. See note [pointwise nat action]. -/
protected def ZSMul [Zero α] [Add α] [Neg α] : SMul ℤ (Set α) :=
  ⟨zsmulRec⟩

Integer scalar multiplication of a set

Informal description

The scalar multiplication of an integer `n` on a set `s` of elements of type `α`, where `α` has zero, addition, and negation operations, is defined as the repeated pointwise addition/subtraction of the set `s` with itself `n` times. Specifically, for `n > 0`, it is the set of all sums of `n` elements from `s`; for `n < 0`, it is the set of all sums of `|n|` negations of elements from `s`; and for `n = 0`, it is the singleton set containing the zero element of `α`.

Set.ZPow definition

[One α] [Mul α] [Inv α] : Pow (Set α) ℤ

Full source

/-- Repeated pointwise multiplication/division (not the same as pointwise repeated
multiplication/division!) of a `Set`. See note [pointwise nat action]. -/
@[to_additive existing]
protected def ZPow [One α] [Mul α] [Inv α] : Pow (Set α) ℤ :=
  ⟨fun s n => zpowRec npowRec n s⟩

Pointwise integer power of a set

Informal description

The pointwise integer power operation on sets, where for a set $s$ in a type $\alpha$ equipped with a multiplicative identity $1$, multiplication, and inversion, and an integer $n$, the set $s^n$ is defined as the set $\{x^n \mid x \in s\}$ using the integer power operation `zpowRec`.

Set.semigroup definition

[Semigroup α] : Semigroup (Set α)

Full source

/-- `Set α` is a `Semigroup` under pointwise operations if `α` is. -/
@[to_additive "`Set α` is an `AddSemigroup` under pointwise operations if `α` is."]
protected noncomputable def semigroup [Semigroup α] : Semigroup (Set α) :=
  { Set.mul with mul_assoc := fun _ _ _ => image2_assoc mul_assoc }

Semigroup structure on sets under pointwise multiplication

Informal description

Given a semigroup $\alpha$, the type `Set α` of sets in $\alpha$ forms a semigroup under pointwise multiplication, where the multiplication of two sets $s$ and $t$ is defined as $\{x \cdot y \mid x \in s, y \in t\}$. The associativity of the semigroup operation on $\alpha$ ensures that this pointwise multiplication is also associative.

Set.commSemigroup definition

: CommSemigroup (Set α)

Full source

/-- `Set α` is a `CommSemigroup` under pointwise operations if `α` is. -/
@[to_additive "`Set α` is an `AddCommSemigroup` under pointwise operations if `α` is."]
protected noncomputable def commSemigroup : CommSemigroup (Set α) :=
  { Set.semigroup with mul_comm := fun _ _ => image2_comm mul_comm }

Commutative semigroup structure on sets under pointwise multiplication

Informal description

Given a commutative semigroup $\alpha$, the type `Set α` of sets in $\alpha$ forms a commutative semigroup under pointwise multiplication, where the multiplication of two sets $s$ and $t$ is defined as $\{x \cdot y \mid x \in s, y \in t\}$. The commutativity of the semigroup operation on $\alpha$ ensures that this pointwise multiplication is also commutative.

Set.inter_mul_union_subset theorem

: s ∩ t * (s ∪ t) ⊆ s * t

Full source

@[to_additive]
theorem inter_mul_union_subset : s ∩ ts ∩ t * (s ∪ t) ⊆ s * t :=
  image2_inter_union_subset mul_comm

Subset property for pointwise product of intersection and union in a commutative semigroup

Informal description

For any sets $s$ and $t$ in a commutative semigroup $\alpha$, the pointwise product of the intersection $s \cap t$ and the union $s \cup t$ is a subset of the pointwise product of $s$ and $t$, i.e., \[ (s \cap t) \cdot (s \cup t) \subseteq s \cdot t. \]

Set.union_mul_inter_subset theorem

: (s ∪ t) * (s ∩ t) ⊆ s * t

Full source

@[to_additive]
theorem union_mul_inter_subset : (s ∪ t) * (s ∩ t) ⊆ s * t :=
  image2_union_inter_subset mul_comm

Subset property for pointwise product of union and intersection in a commutative semigroup

Informal description

For any sets $s$ and $t$ in a commutative semigroup $\alpha$, the pointwise product of the union $s \cup t$ and the intersection $s \cap t$ is a subset of the pointwise product of $s$ and $t$, i.e., $$(s \cup t) \cdot (s \cap t) \subseteq s \cdot t.$$

Set.mulOneClass definition

: MulOneClass (Set α)

Full source

/-- `Set α` is a `MulOneClass` under pointwise operations if `α` is. -/
@[to_additive "`Set α` is an `AddZeroClass` under pointwise operations if `α` is."]
protected noncomputable def mulOneClass : MulOneClass (Set α) :=
  { Set.one, Set.mul with
    mul_one := image2_right_identity mul_one
    one_mul := image2_left_identity one_mul }

Pointwise `MulOneClass` structure on sets

Informal description

The structure `Set α` forms a `MulOneClass` under pointwise operations when `α` is a `MulOneClass`. This means that for any sets `s, t : Set α`, the pointwise multiplication `s * t` is defined as $\{x \cdot y \mid x \in s, y \in t\}$, and the multiplicative identity is the singleton set $\{1\}$. The structure satisfies the axioms `one_mul s = s` and `mul_one s = s` for any set `s`.

Set.subset_mul_left theorem

(s : Set α) {t : Set α} (ht : (1 : α) ∈ t) : s ⊆ s * t

Full source

@[to_additive]
theorem subset_mul_left (s : Set α) {t : Set α} (ht : (1 : α) ∈ t) : s ⊆ s * t := fun x hx =>
  ⟨x, hx, 1, ht, mul_one _⟩

Inclusion of Set in Pointwise Product with Identity-Containing Set

Informal description

For any set $s$ in a type $\alpha$ equipped with a multiplicative monoid structure, and any subset $t$ of $\alpha$ containing the multiplicative identity $1$, the set $s$ is contained in the pointwise product $s \cdot t$.

Set.subset_mul_right theorem

{s : Set α} (t : Set α) (hs : (1 : α) ∈ s) : t ⊆ s * t

Full source

@[to_additive]
theorem subset_mul_right {s : Set α} (t : Set α) (hs : (1 : α) ∈ s) : t ⊆ s * t := fun x hx =>
  ⟨1, hs, x, hx, one_mul _⟩

Right multiplication by a set containing the identity preserves containment

Informal description

For any set $t$ in a type $\alpha$ equipped with a multiplicative identity $1$, if $1$ belongs to a set $s$, then $t$ is a subset of the pointwise product $s \cdot t$.

Set.singletonMonoidHom definition

: α →* Set α

Full source

/-- The singleton operation as a `MonoidHom`. -/
@[to_additive "The singleton operation as an `AddMonoidHom`."]
noncomputable def singletonMonoidHom : α →* Set α :=
  { singletonMulHom, singletonOneHom with }

Singleton monoid homomorphism

Informal description

The function that maps an element $ a $ of a monoid $ \alpha $ to the singleton set $ \{a\} $ is a monoid homomorphism, preserving both the multiplicative operation and the identity element. Specifically, it satisfies: 1. $ \{1\} = 1 $ (where $ 1 $ on the right is the singleton set containing the identity element of $ \alpha $), 2. $ \{a \cdot b\} = \{a\} \cdot \{b\} $ for all $ a, b \in \alpha $.

Set.coe_singletonMonoidHom theorem

: (singletonMonoidHom : α → Set α) = singleton

Full source

@[to_additive (attr := simp)]
theorem coe_singletonMonoidHom : (singletonMonoidHom : α → Set α) = singleton :=
  rfl

Singleton Monoid Homomorphism as Set Constructor

Informal description

The monoid homomorphism that sends an element $a$ of a monoid $\alpha$ to the singleton set $\{a\}$ is equal to the singleton set constructor function.

Set.singletonMonoidHom_apply theorem

(a : α) : singletonMonoidHom a = { a }

Full source

@[to_additive (attr := simp)]
theorem singletonMonoidHom_apply (a : α) : singletonMonoidHom a = {a} :=
  rfl

Singleton Monoid Homomorphism Evaluation: $\text{singletonMonoidHom}(a) = \{a\}$

Informal description

For any element $a$ of a monoid $\alpha$, the monoid homomorphism that sends $a$ to the singleton set $\{a\}$ satisfies $\text{singletonMonoidHom}(a) = \{a\}$.

Set.monoid definition

: Monoid (Set α)

Full source

/-- `Set α` is a `Monoid` under pointwise operations if `α` is. -/
@[to_additive "`Set α` is an `AddMonoid` under pointwise operations if `α` is."]
protected noncomputable def monoid : Monoid (Set α) :=
  { Set.semigroup, Set.mulOneClass, @Set.NPow α _ _ with }

Monoid structure on sets under pointwise operations

Informal description

Given a monoid $\alpha$, the type `Set α` of subsets of $\alpha$ forms a monoid under pointwise operations, where: - The multiplication of two subsets $s$ and $t$ is defined as $\{x \cdot y \mid x \in s, y \in t\}$. - The multiplicative identity is the singleton set $\{1\}$. - The power operation for a natural number $n$ is defined as repeated pointwise multiplication of a set with itself $n$ times. This structure inherits associativity from the semigroup structure on `Set α` and the identity properties from the `MulOneClass` structure.

Set.pow_right_monotone theorem

(hs : 1 ∈ s) : Monotone (s ^ ·)

Full source

@[to_additive]
protected lemma pow_right_monotone (hs : 1 ∈ s) : Monotone (s ^ ·) :=
  pow_right_monotone <| one_subset.2 hs

Monotonicity of Set Powers: $n \mapsto s^n$ is increasing when $1 \in s$

Informal description

For any subset $s$ of a monoid $\alpha$ containing the multiplicative identity $1$, the function $n \mapsto s^n$ is monotone with respect to the subset relation. That is, for any natural numbers $m \leq n$, we have $s^m \subseteq s^n$.

Set.pow_subset_pow_left theorem

(hst : s ⊆ t) : s ^ n ⊆ t ^ n

Full source

@[to_additive (attr := gcongr)]
lemma pow_subset_pow_left (hst : s ⊆ t) : s ^ n ⊆ t ^ n := pow_left_mono _ hst

Monotonicity of Set Powers with Respect to Subset Inclusion

Informal description

For any subsets $s$ and $t$ of a monoid $\alpha$, if $s \subseteq t$, then for any natural number $n$, the $n$-th power of $s$ is contained in the $n$-th power of $t$, i.e., $s^n \subseteq t^n$.

Set.pow_subset_pow_right theorem

(hs : 1 ∈ s) (hmn : m ≤ n) : s ^ m ⊆ s ^ n

Full source

@[to_additive (attr := gcongr)]
lemma pow_subset_pow_right (hs : 1 ∈ s) (hmn : m ≤ n) : s ^ m ⊆ s ^ n :=
  Set.pow_right_monotone hs hmn

Monotonicity of Set Powers: $s^m \subseteq s^n$ for $m \leq n$ when $1 \in s$

Informal description

For any subset $s$ of a monoid $\alpha$ containing the multiplicative identity $1$, and for any natural numbers $m \leq n$, the $m$-th power of $s$ is contained in the $n$-th power of $s$, i.e., $s^m \subseteq s^n$.

Set.pow_subset_pow theorem

(hst : s ⊆ t) (ht : 1 ∈ t) (hmn : m ≤ n) : s ^ m ⊆ t ^ n

Full source

@[to_additive (attr := gcongr)]
lemma pow_subset_pow (hst : s ⊆ t) (ht : 1 ∈ t) (hmn : m ≤ n) : s ^ m ⊆ t ^ n :=
  (pow_subset_pow_left hst).trans (pow_subset_pow_right ht hmn)

Monotonicity of Set Powers: $s^m \subseteq t^n$ for $m \leq n$ when $s \subseteq t$ and $1 \in t$

Informal description

For any subsets $s$ and $t$ of a monoid $\alpha$ such that $s \subseteq t$ and $1 \in t$, and for any natural numbers $m \leq n$, the $m$-th power of $s$ is contained in the $n$-th power of $t$, i.e., $s^m \subseteq t^n$.

Set.subset_pow theorem

(hs : 1 ∈ s) (hn : n ≠ 0) : s ⊆ s ^ n

Full source

@[to_additive]
lemma subset_pow (hs : 1 ∈ s) (hn : n ≠ 0) : s ⊆ s ^ n := by
  simpa using pow_subset_pow_right hs <| Nat.one_le_iff_ne_zero.2 hn

Inclusion of Set in Its Power: $s \subseteq s^n$ for $1 \in s$ and $n \neq 0$

Informal description

For any subset $s$ of a monoid $\alpha$ containing the multiplicative identity $1$, and for any nonzero natural number $n$, the set $s$ is contained in its $n$-th power under pointwise multiplication, i.e., $s \subseteq s^n$.

Set.pow_subset_pow_mul_of_sq_subset_mul theorem

(hst : s ^ 2 ⊆ t * s) (hn : n ≠ 0) : s ^ n ⊆ t ^ (n - 1) * s

Full source

@[to_additive]
lemma pow_subset_pow_mul_of_sq_subset_mul (hst : s ^ 2 ⊆ t * s) (hn : n ≠ 0) :
    s ^ n ⊆ t ^ (n - 1) * s := pow_le_pow_mul_of_sq_le_mul hst hn

Power Subset Inclusion: $s^n \subseteq t^{n-1} \cdot s$ under $s^2 \subseteq t \cdot s$

Informal description

Let $s$ and $t$ be subsets of a monoid $\alpha$ such that $s^2 \subseteq t \cdot s$. Then for any natural number $n \neq 0$, we have $s^n \subseteq t^{n-1} \cdot s$, where $s^n$ denotes the $n$-fold pointwise product of $s$ with itself and $t^{n-1} \cdot s$ denotes the pointwise product of $t^{n-1}$ with $s$.

Set.empty_pow theorem

(hn : n ≠ 0) : (∅ : Set α) ^ n = ∅

Full source

@[to_additive (attr := simp) nsmul_empty]
lemma empty_pow (hn : n ≠ 0) : (∅ : Set α) ^ n = ∅ := match n with | n + 1 => by simp [pow_succ]

Empty Set to Nonzero Power is Empty

Informal description

For any natural number $n \neq 0$, the $n$-th power of the empty set under pointwise multiplication is the empty set, i.e., $\emptyset^n = \emptyset$.

Set.Nonempty.pow theorem

(hs : s.Nonempty) : ∀ {n}, (s ^ n).Nonempty

Full source

@[to_additive]
lemma Nonempty.pow (hs : s.Nonempty) : ∀ {n}, (s ^ n).Nonempty
  | 0 => by simp
  | n + 1 => by rw [pow_succ]; exact hs.pow.mul hs

Nonempty Sets Remain Nonempty Under Powers

Informal description

For any nonempty subset $s$ of a monoid $\alpha$ and any natural number $n$, the $n$-th power set $s^n = \{x^n \mid x \in s\}$ is nonempty.

Set.pow_eq_empty theorem

: s ^ n = ∅ ↔ s = ∅ ∧ n ≠ 0

Full source

@[to_additive (attr := simp)] lemma pow_eq_empty : s ^ n = ∅ ↔ s = ∅ ∧ n ≠ 0 := by
  constructor
  · contrapose!
    rintro (hs | rfl)
    · exact hs.pow
    · simp
  · rintro ⟨rfl, hn⟩
    exact empty_pow hn

Empty Power Set Characterization: $s^n = \emptyset \leftrightarrow (s = \emptyset \land n \neq 0)$

Informal description

For any subset $s$ of a monoid $\alpha$ and any natural number $n$, the $n$-th power set $s^n$ (under pointwise multiplication) is empty if and only if $s$ is empty and $n \neq 0$.

Set.singleton_pow theorem

(a : α) : ∀ n, ({ a } : Set α) ^ n = {a ^ n}

Full source

@[to_additive (attr := simp) nsmul_singleton]
lemma singleton_pow (a : α) : ∀ n, ({a} : Set α) ^ n = {a ^ n}
  | 0 => by simp [singleton_one]
  | n + 1 => by simp [pow_succ, singleton_pow _ n]

Power of Singleton Set: $\{a\}^n = \{a^n\}$

Informal description

For any element $a$ in a monoid $\alpha$ and any natural number $n$, the $n$-th power of the singleton set $\{a\}$ under pointwise multiplication is equal to the singleton set $\{a^n\}$, i.e., $\{a\}^n = \{a^n\}$.

Set.pow_mem_pow theorem

(ha : a ∈ s) : a ^ n ∈ s ^ n

Full source

@[to_additive] lemma pow_mem_pow (ha : a ∈ s) : a ^ n ∈ s ^ n := by
  simpa using pow_subset_pow_left (singleton_subset_iff.2 ha)

Element Power Membership in Set Power: $a^n \in s^n$

Informal description

For any element $a$ in a subset $s$ of a monoid $\alpha$ and any natural number $n$, the $n$-th power of $a$ is contained in the $n$-th power of $s$ under pointwise multiplication, i.e., $a^n \in s^n$.

Set.one_mem_pow theorem

(hs : 1 ∈ s) : 1 ∈ s ^ n

Full source

@[to_additive] lemma one_mem_pow (hs : 1 ∈ s) : 1 ∈ s ^ n := by simpa using pow_mem_pow hs

Preservation of Identity in Set Powers: $1 \in s \Rightarrow 1 \in s^n$

Informal description

For any subset $s$ of a monoid $\alpha$ containing the multiplicative identity $1$, and for any natural number $n$, the identity element $1$ is contained in the $n$-th power of $s$ under pointwise multiplication, i.e., $1 \in s^n$.

Set.inter_pow_subset theorem

: (s ∩ t) ^ n ⊆ s ^ n ∩ t ^ n

Full source

@[to_additive]
lemma inter_pow_subset : (s ∩ t) ^ n ⊆ s ^ n ∩ t ^ n := by apply subset_inter <;> gcongr <;> simp

Inclusion of Powers of Intersection in Intersection of Powers: $(s \cap t)^n \subseteq s^n \cap t^n$

Informal description

For any subsets $s$ and $t$ of a monoid $\alpha$ and any natural number $n$, the $n$-th power of the intersection $s \cap t$ is contained in the intersection of the $n$-th powers of $s$ and $t$, i.e., $(s \cap t)^n \subseteq s^n \cap t^n$.

Set.mul_univ_of_one_mem theorem

(hs : (1 : α) ∈ s) : s * univ = univ

Full source

@[to_additive]
theorem mul_univ_of_one_mem (hs : (1 : α) ∈ s) : s * univ = univ :=
  eq_univ_iff_forall.2 fun _ => mem_mul.2 ⟨_, hs, _, mem_univ _, one_mul _⟩

Pointwise Product with Universal Set when Identity is Present

Informal description

For any set $s$ in a monoid $\alpha$ containing the multiplicative identity $1$, the pointwise product of $s$ with the universal set $\text{univ}$ equals $\text{univ}$. In symbols: $$ 1 \in s \implies s \cdot \text{univ} = \text{univ} $$

Set.univ_mul_of_one_mem theorem

(ht : (1 : α) ∈ t) : univ * t = univ

Full source

@[to_additive]
theorem univ_mul_of_one_mem (ht : (1 : α) ∈ t) : univ * t = univ :=
  eq_univ_iff_forall.2 fun _ => mem_mul.2 ⟨_, mem_univ _, _, ht, mul_one _⟩

Universal Set Multiplied by Set Containing One is Universal

Informal description

For any set $t$ in a monoid $\alpha$ such that the multiplicative identity $1$ is an element of $t$, the pointwise product of the universal set $\text{univ}$ and $t$ equals $\text{univ}$. In symbols: $$ \text{univ} \cdot t = \text{univ} \quad \text{whenever} \quad 1 \in t. $$

Set.univ_mul_univ theorem

: (univ : Set α) * univ = univ

Full source

@[to_additive (attr := simp)]
theorem univ_mul_univ : (univ : Set α) * univ = univ :=
  mul_univ_of_one_mem <| mem_univ _

Universal Set is Closed Under Pointwise Multiplication

Informal description

For any monoid $\alpha$, the pointwise product of the universal set $\text{univ}$ with itself equals $\text{univ}$. In symbols: $$\text{univ} \cdot \text{univ} = \text{univ}$$

Set.univ_pow theorem

: ∀ {n : ℕ}, n ≠ 0 → (univ : Set α) ^ n = univ

Full source

@[to_additive (attr := simp) nsmul_univ]
theorem univ_pow : ∀ {n : ℕ}, n ≠ 0 → (univ : Set α) ^ n = univ
  | 0 => fun h => (h rfl).elim
  | 1 => fun _ => pow_one _
  | n + 2 => fun _ => by rw [pow_succ, univ_pow n.succ_ne_zero, univ_mul_univ]

Universal Set is Closed Under Nonzero Powers: $\text{univ}^n = \text{univ}$ for $n \neq 0$

Informal description

For any natural number $n \neq 0$ and any monoid $\alpha$, the $n$-th power of the universal set $\text{univ} \subseteq \alpha$ under pointwise multiplication equals $\text{univ}$ itself. In symbols: $$\text{univ}^n = \text{univ} \quad \text{for all} \quad n \in \mathbb{N} \setminus \{0\}.$$

IsUnit.set theorem

: IsUnit a → IsUnit ({ a } : Set α)

Full source

@[to_additive]
protected theorem _root_.IsUnit.set : IsUnit a → IsUnit ({a} : Set α) :=
  IsUnit.map (singletonMonoidHom : α →* Set α)

Singleton Set of a Unit is a Unit in the Pointwise Monoid of Sets

Informal description

If an element $a$ of a monoid $\alpha$ is a unit (i.e., has a multiplicative inverse), then the singleton set $\{a\}$ is a unit in the monoid of subsets of $\alpha$ under pointwise multiplication.

Set.prod_pow theorem

[Monoid β] (s : Set α) (t : Set β) : ∀ n, (s ×ˢ t) ^ n = (s ^ n) ×ˢ (t ^ n)

Full source

@[to_additive nsmul_prod]
lemma prod_pow [Monoid β] (s : Set α) (t : Set β) : ∀ n, (s ×ˢ t) ^ n = (s ^ n) ×ˢ (t ^ n)
  | 0 => by simp
  | n + 1 => by simp [pow_succ, prod_pow _ _ n]

Power of Cartesian Product Equals Cartesian Product of Powers: $(s \times t)^n = s^n \times t^n$

Informal description

Let $\alpha$ and $\beta$ be types equipped with monoid structures. For any subsets $s \subseteq \alpha$ and $t \subseteq \beta$, and for any natural number $n$, the $n$-th power of the Cartesian product $s \times t$ under pointwise multiplication equals the Cartesian product of the $n$-th powers of $s$ and $t$, i.e., $$(s \times t)^n = s^n \times t^n.$$

Set.Nontrivial.mul_left theorem

: t.Nontrivial → s.Nonempty → (s * t).Nontrivial

Full source

@[to_additive]
lemma Nontrivial.mul_left : t.Nontrivial → s.Nonempty → (s * t).Nontrivial := by
  rintro ⟨a, ha, b, hb, hab⟩ ⟨c, hc⟩
  exact ⟨c * a, mul_mem_mul hc ha, c * b, mul_mem_mul hc hb, by simpa⟩

Nontriviality of Pointwise Product under Nontrivial Right Factor and Nonempty Left Factor

Informal description

Let $s$ and $t$ be sets in a type $\alpha$ equipped with a multiplication operation. If $t$ is nontrivial (contains at least two distinct elements) and $s$ is nonempty (contains at least one element), then the pointwise product set $s \cdot t$ is also nontrivial.

Set.Nontrivial.mul theorem

(hs : s.Nontrivial) (ht : t.Nontrivial) : (s * t).Nontrivial

Full source

@[to_additive]
lemma Nontrivial.mul (hs : s.Nontrivial) (ht : t.Nontrivial) : (s * t).Nontrivial :=
  ht.mul_left hs.nonempty

Nontriviality of Pointwise Product of Nontrivial Sets

Informal description

For any two nontrivial sets $s$ and $t$ in a type $\alpha$ equipped with a multiplication operation, the pointwise product set $s \cdot t$ is also nontrivial. Here, a set is called *nontrivial* if it contains at least two distinct elements.

Set.Nontrivial.mul_right theorem

: s.Nontrivial → t.Nonempty → (s * t).Nontrivial

Full source

@[to_additive]
lemma Nontrivial.mul_right : s.Nontrivial → t.Nonempty → (s * t).Nontrivial := by
  rintro ⟨a, ha, b, hb, hab⟩ ⟨c, hc⟩
  exact ⟨a * c, mul_mem_mul ha hc, b * c, mul_mem_mul hb hc, by simpa⟩

Nontriviality of Pointwise Product under Right Multiplication

Informal description

For any two sets $s$ and $t$ in a type $\alpha$ equipped with a multiplication operation, if $s$ is nontrivial (i.e., contains at least two distinct elements) and $t$ is nonempty (i.e., contains at least one element), then the pointwise product set $s \cdot t$ is also nontrivial.

Set.Nontrivial.pow theorem

(hs : s.Nontrivial) : ∀ {n}, n ≠ 0 → (s ^ n).Nontrivial

Full source

@[to_additive]
lemma Nontrivial.pow (hs : s.Nontrivial) : ∀ {n}, n ≠ 0 → (s ^ n).Nontrivial
  | 1, _ => by simpa
  | n + 2, _ => by simpa [pow_succ] using (hs.pow n.succ_ne_zero).mul hs

Nontriviality of Pointwise Powers of Nontrivial Sets: $s^n$ is nontrivial for $n \neq 0$

Informal description

For any nontrivial set $s$ in a monoid $\alpha$ (i.e., $s$ contains at least two distinct elements) and any nonzero natural number $n$, the $n$-th pointwise power $s^n$ is also nontrivial.

Set.commMonoid definition

[CommMonoid α] : CommMonoid (Set α)

Full source

/-- `Set α` is a `CommMonoid` under pointwise operations if `α` is. -/
@[to_additive "`Set α` is an `AddCommMonoid` under pointwise operations if `α` is."]
protected noncomputable def commMonoid [CommMonoid α] : CommMonoid (Set α) :=
  { Set.monoid, Set.commSemigroup with }

Commutative monoid structure on sets under pointwise operations

Informal description

Given a commutative monoid $\alpha$, the type `Set α` of subsets of $\alpha$ forms a commutative monoid under pointwise operations, where: - The multiplication of two subsets $s$ and $t$ is defined as $\{x \cdot y \mid x \in s, y \in t\}$. - The multiplicative identity is the singleton set $\{1\}$. - The commutativity of the monoid operation on $\alpha$ ensures that this pointwise multiplication is also commutative.

Set.mul_eq_one_iff theorem

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

Full source

@[to_additive]
protected theorem mul_eq_one_iff : s * t = 1 ↔ ∃ a b, s = {a} ∧ t = {b} ∧ a * b = 1 := by
  refine ⟨fun h => ?_, ?_⟩
  · have hst : (s * t).Nonempty := h.symm.subst one_nonempty
    obtain ⟨a, ha⟩ := hst.of_image2_left
    obtain ⟨b, hb⟩ := hst.of_image2_right
    have H : ∀ {a b}, a ∈ s → b ∈ t → a * b = (1 : α) := fun {a b} ha hb =>
      h.subset <| mem_image2_of_mem ha hb
    refine ⟨a, b, ?_, ?_, H ha hb⟩ <;> refine eq_singleton_iff_unique_mem.2 ⟨‹_›, fun x hx => ?_⟩
    · exact (eq_inv_of_mul_eq_one_left <| H hx hb).trans (inv_eq_of_mul_eq_one_left <| H ha hb)
    · exact (eq_inv_of_mul_eq_one_right <| H ha hx).trans (inv_eq_of_mul_eq_one_right <| H ha hb)
  · rintro ⟨b, c, rfl, rfl, h⟩
    rw [singleton_mul_singleton, h, singleton_one]

Characterization of Pointwise Product as Identity: $s \cdot t = \{1\} \iff \exists a b, s = \{a\} \land t = \{b\} \land a \cdot b = 1$

Informal description

For any two subsets $s$ and $t$ of a division monoid $\alpha$, the pointwise product $s \cdot t$ equals the singleton set $\{1\}$ if and only if there exist elements $a, b \in \alpha$ such that $s = \{a\}$, $t = \{b\}$, and $a \cdot b = 1$.

Set.divisionMonoid definition

: DivisionMonoid (Set α)

Full source

/-- `Set α` is a division monoid under pointwise operations if `α` is. -/
@[to_additive
    "`Set α` is a subtraction monoid under pointwise operations if `α` is."]
protected noncomputable def divisionMonoid : DivisionMonoid (Set α) :=
  { Set.monoid, Set.involutiveInv, Set.div, @Set.ZPow α _ _ _ with
    mul_inv_rev := fun s t => by
      simp_rw [← image_inv_eq_inv]
      exact image_image2_antidistrib mul_inv_rev
    inv_eq_of_mul := fun s t h => by
      obtain ⟨a, b, rfl, rfl, hab⟩ := Set.mul_eq_one_iff.1 h
      rw [inv_singleton, inv_eq_of_mul_eq_one_right hab]
    div_eq_mul_inv := fun s t => by
      rw [← image_id (s / t), ← image_inv_eq_inv]
      exact image_image2_distrib_right div_eq_mul_inv }

Division monoid structure on sets under pointwise operations

Informal description

Given a type $\alpha$ equipped with a division monoid structure, the collection of all subsets of $\alpha$ forms a division monoid under pointwise operations. Specifically: - The multiplication of two subsets $s$ and $t$ is defined as $\{x \cdot y \mid x \in s, y \in t\}$. - The inversion of a subset $s$ is defined as $\{x^{-1} \mid x \in s\}$. - The division of two subsets $s$ and $t$ is defined as $\{x / y \mid x \in s, y \in t\}$. - The structure satisfies the properties: - $(s \cdot t)^{-1} = t^{-1} \cdot s^{-1}$. - If $s \cdot t = \{1\}$, then $s^{-1} = t$. - $s / t = s \cdot t^{-1}$.

Set.isUnit_iff theorem

: IsUnit s ↔ ∃ a, s = { a } ∧ IsUnit a

Full source

@[to_additive (attr := simp 500)]
theorem isUnit_iff : IsUnitIsUnit s ↔ ∃ a, s = {a} ∧ IsUnit a := by
  constructor
  · rintro ⟨u, rfl⟩
    obtain ⟨a, b, ha, hb, h⟩ := Set.mul_eq_one_iff.1 u.mul_inv
    refine ⟨a, ha, ⟨a, b, h, singleton_injective ?_⟩, rfl⟩
    rw [← singleton_mul_singleton, ← ha, ← hb]
    exact u.inv_mul
  · rintro ⟨a, rfl, ha⟩
    exact ha.set

Characterization of Units in the Pointwise Monoid of Sets: $s$ is a unit $\iff$ $s = \{a\}$ for some unit $a$

Informal description

A subset $s$ of a division monoid $\alpha$ is a unit in the pointwise monoid of sets if and only if $s$ is a singleton set $\{a\}$ for some unit $a \in \alpha$.

Set.univ_div_univ theorem

: (univ / univ : Set α) = univ

Full source

@[to_additive (attr := simp)]
lemma univ_div_univ : (univ / univ : Set α) = univ := by simp [div_eq_mul_inv]

Universal Set is Closed Under Pointwise Division

Informal description

For any type $\alpha$ equipped with a division operation, the pointwise division of the universal set $\text{univ}$ by itself equals $\text{univ}$. In symbols: $$\text{univ} / \text{univ} = \text{univ}$$

Set.subset_div_left theorem

(ht : 1 ∈ t) : s ⊆ s / t

Full source

@[to_additive] lemma subset_div_left (ht : 1 ∈ t) : s ⊆ s / t := by
  rw [div_eq_mul_inv]; exact subset_mul_left _ <| by simpa

Inclusion of Set in Pointwise Division by Identity-Containing Set

Informal description

For any subset $t$ of a division monoid $\alpha$ containing the multiplicative identity $1$, and for any subset $s$ of $\alpha$, we have $s \subseteq s / t$, where $s / t$ denotes the pointwise division $\{x / y \mid x \in s, y \in t\}$.

Set.inv_subset_div_right theorem

(hs : 1 ∈ s) : t⁻¹ ⊆ s / t

Full source

@[to_additive] lemma inv_subset_div_right (hs : 1 ∈ s) : t⁻¹t⁻¹ ⊆ s / t := by
  rw [div_eq_mul_inv]; exact subset_mul_right _ hs

Inverse Subset in Division by a Set Containing Identity

Informal description

For any subset $t$ of a division monoid $\alpha$, if the multiplicative identity $1$ belongs to a subset $s$, then the pointwise inverse $t^{-1}$ is contained in the pointwise division $s / t$.

Set.empty_zpow theorem

(hn : n ≠ 0) : (∅ : Set α) ^ n = ∅

Full source

@[to_additive (attr := simp) zsmul_empty]
lemma empty_zpow (hn : n ≠ 0) : (∅ : Set α) ^ n = ∅ := by cases n <;> aesop

Empty Set to Nonzero Integer Power is Empty

Informal description

For any integer $n \neq 0$, the pointwise integer power of the empty set $\emptyset$ in a type $\alpha$ is the empty set, i.e., $\emptyset^n = \emptyset$.

Set.Nonempty.zpow theorem

(hs : s.Nonempty) : ∀ {n : ℤ}, (s ^ n).Nonempty

Full source

@[to_additive]
lemma Nonempty.zpow (hs : s.Nonempty) : ∀ {n : ℤ}, (s ^ n).Nonempty
  | (n : ℕ) => hs.pow
  | .negSucc n => by simpa using hs.pow

Nonempty Sets Remain Nonempty Under Pointwise Integer Powers

Informal description

For any nonempty subset $s$ of a type $\alpha$ equipped with a division monoid structure and any integer $n$, the pointwise power set $s^n = \{x^n \mid x \in s\}$ is nonempty.

Set.zpow_eq_empty theorem

: s ^ n = ∅ ↔ s = ∅ ∧ n ≠ 0

Full source

@[to_additive (attr := simp)] lemma zpow_eq_empty : s ^ n = ∅ ↔ s = ∅ ∧ n ≠ 0 := by
  constructor
  · contrapose!
    rintro (hs | rfl)
    · exact hs.zpow
    · simp
  · rintro ⟨rfl, hn⟩
    exact empty_zpow hn

Empty Set Condition for Pointwise Integer Powers: $s^n = \emptyset \leftrightarrow (s = \emptyset \land n \neq 0)$

Informal description

For a set $s$ in a type $\alpha$ equipped with a division monoid structure and an integer $n$, the pointwise power set $s^n$ is empty if and only if $s$ is empty and $n$ is nonzero, i.e., $s^n = \emptyset \leftrightarrow (s = \emptyset \land n \neq 0)$.

Set.singleton_zpow theorem

(a : α) (n : ℤ) : ({ a } : Set α) ^ n = {a ^ n}

Full source

@[to_additive (attr := simp) zsmul_singleton]
lemma singleton_zpow (a : α) (n : ℤ) : ({a} : Set α) ^ n = {a ^ n} := by cases n <;> simp

Pointwise Integer Power of Singleton Set: $\{a\}^n = \{a^n\}$

Informal description

For any element $a$ in a type $\alpha$ equipped with a division monoid structure and any integer $n$, the pointwise integer power of the singleton set $\{a\}$ is equal to the singleton set $\{a^n\}$, i.e., $\{a\}^n = \{a^n\}$.

Set.divisionCommMonoid definition

[DivisionCommMonoid α] : DivisionCommMonoid (Set α)

Full source

/-- `Set α` is a commutative division monoid under pointwise operations if `α` is. -/
@[to_additive subtractionCommMonoid
      "`Set α` is a commutative subtraction monoid under pointwise operations if `α` is."]
protected noncomputable def divisionCommMonoid [DivisionCommMonoid α] :
    DivisionCommMonoid (Set α) :=
  { Set.divisionMonoid, Set.commSemigroup with }

Commutative division monoid structure on sets under pointwise operations

Informal description

Given a commutative division monoid $\alpha$, the collection of all subsets of $\alpha$ forms a commutative division monoid under pointwise operations. Specifically: - The multiplication of two subsets $s$ and $t$ is defined as $\{x \cdot y \mid x \in s, y \in t\}$. - The inversion of a subset $s$ is defined as $\{x^{-1} \mid x \in s\}$. - The division of two subsets $s$ and $t$ is defined as $\{x / y \mid x \in s, y \in t\}$. - The structure satisfies the properties: - $(s \cdot t)^{-1} = t^{-1} \cdot s^{-1}$. - If $s \cdot t = \{1\}$, then $s^{-1} = t$. - $s / t = s \cdot t^{-1}$.

Set.one_mem_div_iff theorem

: (1 : α) ∈ s / t ↔ ¬Disjoint s t

Full source

@[to_additive (attr := simp)]
theorem one_mem_div_iff : (1 : α) ∈ s / t(1 : α) ∈ s / t ↔ ¬Disjoint s t := by
  simp [not_disjoint_iff_nonempty_inter, mem_div, div_eq_one, Set.Nonempty]

Membership of Identity in Pointwise Division Set Characterizes Non-Disjointness

Informal description

For any two sets $s$ and $t$ in a group $\alpha$, the multiplicative identity $1$ belongs to the pointwise division set $s / t$ if and only if $s$ and $t$ are not disjoint (i.e., there exists an element $x \in s \cap t$).

Set.one_mem_inv_mul_iff theorem

: (1 : α) ∈ t⁻¹ * s ↔ ¬Disjoint s t

Full source

@[to_additive (attr := simp)]
lemma one_mem_inv_mul_iff : (1 : α) ∈ t⁻¹ * s(1 : α) ∈ t⁻¹ * s ↔ ¬Disjoint s t := by
  aesop (add simp [not_disjoint_iff_nonempty_inter, mem_mul, mul_eq_one_iff_eq_inv, Set.Nonempty])

Membership of Identity in Inverted Set Product: $1 \in t^{-1} * s \leftrightarrow s \cap t \neq \emptyset$

Informal description

For any two sets $s$ and $t$ in a group $\alpha$, the multiplicative identity $1$ belongs to the pointwise product $t^{-1} * s$ if and only if $s$ and $t$ are not disjoint (i.e., $s \cap t \neq \emptyset$).

Set.not_one_mem_div_iff theorem

: (1 : α) ∉ s / t ↔ Disjoint s t

Full source

@[to_additive]
theorem not_one_mem_div_iff : (1 : α) ∉ s / t(1 : α) ∉ s / t ↔ Disjoint s t :=
  one_mem_div_iff.not_left

Characterization of Disjoint Sets via Pointwise Division: $1 \notin s / t \leftrightarrow s \cap t = \emptyset$

Informal description

For any two sets $s$ and $t$ in a group $\alpha$, the multiplicative identity $1$ does not belong to the pointwise division set $s / t$ if and only if $s$ and $t$ are disjoint (i.e., $s \cap t = \emptyset$).

Set.not_one_mem_inv_mul_iff theorem

: (1 : α) ∉ t⁻¹ * s ↔ Disjoint s t

Full source

@[to_additive]
lemma not_one_mem_inv_mul_iff : (1 : α) ∉ t⁻¹ * s(1 : α) ∉ t⁻¹ * s ↔ Disjoint s t := one_mem_inv_mul_iff.not_left

Disjointness Criterion via Inverted Set Product: $1 \notin t^{-1} * s \leftrightarrow s \cap t = \emptyset$

Informal description

For any two sets $s$ and $t$ in a group $\alpha$, the multiplicative identity $1$ does not belong to the pointwise product $t^{-1} * s$ if and only if $s$ and $t$ are disjoint (i.e., $s \cap t = \emptyset$).

Set.Nonempty.one_mem_div theorem

(h : s.Nonempty) : (1 : α) ∈ s / s

Full source

@[to_additive]
theorem Nonempty.one_mem_div (h : s.Nonempty) : (1 : α) ∈ s / s :=
  let ⟨a, ha⟩ := h
  mem_div.2 ⟨a, ha, a, ha, div_self' _⟩

Identity Element in Division of Nonempty Set by Itself

Informal description

For any nonempty set $s$ in a group $\alpha$, the identity element $1$ belongs to the pointwise division of $s$ by itself, i.e., $1 \in s / s$.

Set.isUnit_singleton theorem

(a : α) : IsUnit ({ a } : Set α)

Full source

@[to_additive]
theorem isUnit_singleton (a : α) : IsUnit ({a} : Set α) :=
  (Group.isUnit a).set

Singleton Sets are Units in Pointwise Monoid of Sets

Informal description

For any element $a$ in a group $\alpha$, the singleton set $\{a\}$ is a unit in the monoid of subsets of $\alpha$ under pointwise multiplication.

Set.isUnit_iff_singleton theorem

: IsUnit s ↔ ∃ a, s = { a }

Full source

@[to_additive (attr := simp)]
theorem isUnit_iff_singleton : IsUnitIsUnit s ↔ ∃ a, s = {a} := by
  simp only [isUnit_iff, Group.isUnit, and_true]

Characterization of unit sets in a group: $s$ is a unit if and only if $s$ is a singleton

Informal description

A subset $s$ of a group $\alpha$ is a unit in the monoid of sets under pointwise multiplication if and only if $s$ is a singleton set, i.e., there exists an element $a \in \alpha$ such that $s = \{a\}$.

Set.image_mul_left theorem

: (a * ·) '' t = (a⁻¹ * ·) ⁻¹' t

Full source

@[to_additive (attr := simp)]
theorem image_mul_left : (a * ·) '' t = (a⁻¹ * ·) ⁻¹' t := by
  rw [image_eq_preimage_of_inverse] <;> intro c <;> simp

Image of Set under Left Multiplication Equals Preimage under Inverse Left Multiplication

Informal description

For any element $a$ in a group $G$ and any subset $t \subseteq G$, the image of $t$ under left multiplication by $a$ is equal to the preimage of $t$ under left multiplication by $a^{-1}$. In other words, \[ \{a \cdot x \mid x \in t\} = \{y \in G \mid a^{-1} \cdot y \in t\}. \]

Set.image_mul_right theorem

: (· * b) '' t = (· * b⁻¹) ⁻¹' t

Full source

@[to_additive (attr := simp)]
theorem image_mul_right : (· * b) '' t = (· * b⁻¹) ⁻¹' t := by
  rw [image_eq_preimage_of_inverse] <;> intro c <;> simp

Right Multiplication Image-Preimage Duality: $(· * b)(t) = (· * b⁻¹)^{-1}(t)$

Informal description

For any element $b$ in a group $G$ and any subset $t \subseteq G$, the image of $t$ under right multiplication by $b$ is equal to the preimage of $t$ under right multiplication by $b^{-1}$. In other words: $$ \{x * b \mid x \in t\} = \{y \mid y * b^{-1} \in t\} $$

Set.image_mul_left' theorem

: (a⁻¹ * ·) '' t = (a * ·) ⁻¹' t

Full source

@[to_additive]
theorem image_mul_left' : (a⁻¹ * ·) '' t = (a * ·) ⁻¹' t := by simp

Image-Preimage Duality under Left Multiplication: $(a^{-1} \cdot \cdot)(t) = (a \cdot \cdot)^{-1}(t)$

Informal description

For any element $a$ in a group $G$ and any subset $t \subseteq G$, the image of $t$ under left multiplication by $a^{-1}$ is equal to the preimage of $t$ under left multiplication by $a$. In other words, \[ \{a^{-1} \cdot x \mid x \in t\} = \{y \in G \mid a \cdot y \in t\}. \]

Set.image_mul_right' theorem

: (· * b⁻¹) '' t = (· * b) ⁻¹' t

Full source

@[to_additive]
theorem image_mul_right' : (· * b⁻¹) '' t = (· * b) ⁻¹' t := by simp

Image-Preimage Duality under Right Multiplication: $(· * b^{-1})(t) = (· * b)^{-1}(t)$

Informal description

For any element $b$ in a group $G$ and any subset $t \subseteq G$, the image of $t$ under right multiplication by $b^{-1}$ is equal to the preimage of $t$ under right multiplication by $b$. In other words: $$ \{x * b^{-1} \mid x \in t\} = \{y \in G \mid y * b \in t\} $$

Set.preimage_mul_left_singleton theorem

: (a * ·) ⁻¹' { b } = {a⁻¹ * b}

Full source

@[to_additive (attr := simp)]
theorem preimage_mul_left_singleton : (a * ·) ⁻¹' {b} = {a⁻¹ * b} := by
  rw [← image_mul_left', image_singleton]

Preimage of Singleton under Left Multiplication: $(a \cdot \cdot)^{-1}(\{b\}) = \{a^{-1}b\}$

Informal description

For any elements $a$ and $b$ in a group $G$, the preimage of the singleton set $\{b\}$ under the left multiplication map $x \mapsto a \cdot x$ is the singleton set $\{a^{-1} \cdot b\}$. In other words: $$ \{x \in G \mid a \cdot x = b\} = \{a^{-1} \cdot b\} $$

Set.preimage_mul_right_singleton theorem

: (· * a) ⁻¹' { b } = {b * a⁻¹}

Full source

@[to_additive (attr := simp)]
theorem preimage_mul_right_singleton : (· * a) ⁻¹' {b} = {b * a⁻¹} := by
  rw [← image_mul_right', image_singleton]

Preimage of Singleton under Right Multiplication: $\{x \mid x * a = b\} = \{b * a^{-1}\}$

Informal description

For any elements $a$ and $b$ in a group $G$, the preimage of the singleton set $\{b\}$ under the right multiplication map $x \mapsto x * a$ is the singleton set $\{b * a^{-1}\}$. In other words: $$ \{x \in G \mid x * a = b\} = \{b * a^{-1}\} $$

Set.preimage_mul_left_one theorem

: (a * ·) ⁻¹' 1 = {a⁻¹}

Full source

@[to_additive (attr := simp)]
theorem preimage_mul_left_one : (a * ·) ⁻¹' 1 = {a⁻¹} := by
  rw [← image_mul_left', image_one, mul_one]

Preimage of Identity under Left Multiplication by $a$ is $\{a^{-1}\}$

Informal description

For any element $a$ in a group $G$, the preimage of the singleton set $\{1\}$ under the left multiplication map $x \mapsto a \cdot x$ is the singleton set $\{a^{-1}\}$. In other words, \[ \{x \in G \mid a \cdot x = 1\} = \{a^{-1}\}. \]

Set.preimage_mul_right_one theorem

: (· * b) ⁻¹' 1 = {b⁻¹}

Full source

@[to_additive (attr := simp)]
theorem preimage_mul_right_one : (· * b) ⁻¹' 1 = {b⁻¹} := by
  rw [← image_mul_right', image_one, one_mul]

Preimage of Identity under Right Multiplication: $(· * b)^{-1}(\{1\}) = \{b^{-1}\}$

Informal description

For any element $b$ in a group $G$, the preimage of the multiplicative identity set $\{1\}$ under the right multiplication map $x \mapsto x * b$ is the singleton set $\{b^{-1}\}$. In other words: $$ \{x \in G \mid x * b = 1\} = \{b^{-1}\} $$

Set.preimage_mul_left_one' theorem

: (a⁻¹ * ·) ⁻¹' 1 = { a }

Full source

@[to_additive]
theorem preimage_mul_left_one' : (a⁻¹ * ·) ⁻¹' 1 = {a} := by simp

Preimage of Identity under Left Multiplication by $a^{-1}$ is $\{a\}$

Informal description

For any element $a$ in a group $G$, the preimage of the singleton set $\{1\}$ under the left multiplication map $x \mapsto a^{-1} \cdot x$ is the singleton set $\{a\}$. In other words, \[ \{x \in G \mid a^{-1} \cdot x = 1\} = \{a\}. \]

Set.preimage_mul_right_one' theorem

: (· * b⁻¹) ⁻¹' 1 = { b }

Full source

@[to_additive]
theorem preimage_mul_right_one' : (· * b⁻¹) ⁻¹' 1 = {b} := by simp

Preimage of Identity under Right Multiplication by Inverse: $(· * b^{-1})^{-1}(\{1\}) = \{b\}$

Informal description

For any element $b$ in a group $G$, the preimage of the multiplicative identity set $\{1\}$ under the right multiplication map $x \mapsto x * b^{-1}$ is the singleton set $\{b\}$. In other words: $$ \{x \in G \mid x * b^{-1} = 1\} = \{b\} $$

Set.mul_univ theorem

(hs : s.Nonempty) : s * (univ : Set α) = univ

Full source

@[to_additive (attr := simp)]
theorem mul_univ (hs : s.Nonempty) : s * (univ : Set α) = univ :=
  let ⟨a, ha⟩ := hs
  eq_univ_of_forall fun b => ⟨a, ha, a⁻¹ * b, trivial, mul_inv_cancel_left ..⟩

Nonempty Set Absorbs Universal Set Under Pointwise Multiplication

Informal description

For any nonempty set $s$ in a type $\alpha$ equipped with a multiplication operation, the pointwise product of $s$ with the universal set (containing all elements of $\alpha$) is equal to the universal set. That is, $s \cdot \mathrm{univ} = \mathrm{univ}$.

Set.univ_mul theorem

(ht : t.Nonempty) : (univ : Set α) * t = univ

Full source

@[to_additive (attr := simp)]
theorem univ_mul (ht : t.Nonempty) : (univ : Set α) * t = univ :=
  let ⟨a, ha⟩ := ht
  eq_univ_of_forall fun b => ⟨b * a⁻¹, trivial, a, ha, inv_mul_cancel_right ..⟩

Universal Set Absorbs Nonempty Set Under Pointwise Multiplication

Informal description

For any nonempty set $t$ in a type $\alpha$ equipped with a multiplication operation, the pointwise product of the universal set (containing all elements of $\alpha$) with $t$ is equal to the universal set. That is, $\mathrm{univ} \cdot t = \mathrm{univ}$.

Set.image_inv theorem

[DivisionMonoid β] [FunLike F α β] [MonoidHomClass F α β] (f : F) (s : Set α) : f '' s⁻¹ = (f '' s)⁻¹

Full source

@[to_additive]
lemma image_inv [DivisionMonoid β] [FunLike F α β] [MonoidHomClass F α β] (f : F) (s : Set α) :
    f '' s⁻¹ = (f '' s)⁻¹ := by
  rw [← image_inv_eq_inv, ← image_inv_eq_inv]; exact image_comm (map_inv _)

Image of Pointwise Inverse Equals Pointwise Inverse of Image under Monoid Homomorphism

Informal description

Let $\alpha$ and $\beta$ be types where $\beta$ is a division monoid. Given a monoid homomorphism $f \colon \alpha \to \beta$ and a subset $s \subseteq \alpha$, the image of the pointwise inverse set $f(s^{-1})$ is equal to the pointwise inverse of the image $(f(s))^{-1}$. In other words, $f(\{x^{-1} \mid x \in s\}) = \{f(x)^{-1} \mid x \in s\}$.

Set.image_mul theorem

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

Full source

@[to_additive]
theorem image_mul : m '' (s * t) = m '' s * m '' t :=
  image_image2_distrib <| map_mul m

Image of Pointwise Product Equals Pointwise Product of Images

Informal description

For any function $m \colon \alpha \to \beta$ and subsets $s, t \subseteq \alpha$, the image of the pointwise product set $s \cdot t$ under $m$ is equal to the pointwise product of the images $m(s)$ and $m(t)$. That is, \[ m(s \cdot t) = m(s) \cdot m(t). \]

Set.mul_subset_range theorem

{s t : Set β} (hs : s ⊆ range m) (ht : t ⊆ range m) : s * t ⊆ range m

Full source

@[to_additive]
lemma mul_subset_range {s t : Set β} (hs : s ⊆ range m) (ht : t ⊆ range m) : s * t ⊆ range m := by
  rintro _ ⟨a, ha, b, hb, rfl⟩
  obtain ⟨a, rfl⟩ := hs ha
  obtain ⟨b, rfl⟩ := ht hb
  exact ⟨a * b, map_mul ..⟩

Range Closure under Pointwise Multiplication

Informal description

For any subsets $s$ and $t$ of a type $\beta$ equipped with a multiplication operation, if $s$ and $t$ are both subsets of the range of a function $m$, then their pointwise product $s * t$ is also a subset of the range of $m$.

Set.preimage_mul_preimage_subset theorem

{s t : Set β} : m ⁻¹' s * m ⁻¹' t ⊆ m ⁻¹' (s * t)

Full source

@[to_additive]
theorem preimage_mul_preimage_subset {s t : Set β} : m ⁻¹' sm ⁻¹' s * m ⁻¹' t ⊆ m ⁻¹' (s * t) := by
  rintro _ ⟨_, _, _, _, rfl⟩
  exact ⟨_, ‹_›, _, ‹_›, (map_mul m ..).symm⟩

Preimage of Product Set Contains Product of Preimages

Informal description

For any sets $s, t \subseteq \beta$ and a function $m : \alpha \to \beta$, the pointwise product of the preimages $m^{-1}(s) * m^{-1}(t)$ is a subset of the preimage of the pointwise product $m^{-1}(s * t)$. In other words, if $x \in m^{-1}(s)$ and $y \in m^{-1}(t)$, then $x * y \in m^{-1}(s * t)$.

Set.preimage_mul theorem

 (hm : Injective m) {s t : Set β} (hs : s ⊆ range m) (ht : t ⊆ range m) : m ⁻¹' (s * t) = m ⁻¹' s * m ⁻¹' t

Full source

@[to_additive]
lemma preimage_mul (hm : Injective m) {s t : Set β} (hs : s ⊆ range m) (ht : t ⊆ range m) :
    m ⁻¹' (s * t) = m ⁻¹' s * m ⁻¹' t :=
  hm.image_injective <| by
    rw [image_mul, image_preimage_eq_iff.2 hs, image_preimage_eq_iff.2 ht,
      image_preimage_eq_iff.2 (mul_subset_range m hs ht)]

Preimage of Pointwise Product under Injective Function

Informal description

Let $m : \alpha \to \beta$ be an injective function, and let $s, t \subseteq \beta$ be subsets contained in the range of $m$. Then the preimage of the pointwise product set $s \cdot t$ under $m$ is equal to the pointwise product of the preimages: \[ m^{-1}(s \cdot t) = m^{-1}(s) \cdot m^{-1}(t). \]

Set.image_pow_of_ne_zero theorem

[MulHomClass F α β] : ∀ {n}, n ≠ 0 → ∀ (f : F) (s : Set α), f '' (s ^ n) = (f '' s) ^ n

Full source

@[to_additive]
lemma image_pow_of_ne_zero [MulHomClass F α β] :
    ∀ {n}, n ≠ 0 → ∀ (f : F) (s : Set α), f '' (s ^ n) = (f '' s) ^ n
  | 1, _ => by simp
  | n + 2, _ => by simp [image_mul, pow_succ _ n.succ, image_pow_of_ne_zero]

Image of Set Power under Multiplication-Preserving Homomorphism for Nonzero Powers

Informal description

Let $\alpha$ and $\beta$ be types equipped with multiplication operations, and let $F$ be a type of homomorphisms from $\alpha$ to $\beta$ that preserve multiplication. For any nonzero natural number $n \neq 0$, any homomorphism $f \in F$, and any subset $s \subseteq \alpha$, the image of the $n$-th power of $s$ under $f$ is equal to the $n$-th power of the image of $s$ under $f$. That is, \[ f(s^n) = (f(s))^n. \]

Set.image_pow theorem

[MonoidHomClass F α β] (f : F) (s : Set α) : ∀ n, f '' (s ^ n) = (f '' s) ^ n

Full source

@[to_additive]
lemma image_pow [MonoidHomClass F α β] (f : F) (s : Set α) : ∀ n, f '' (s ^ n) = (f '' s) ^ n
  | 0 => by simp [singleton_one]
  | n + 1 => image_pow_of_ne_zero n.succ_ne_zero ..

Image of Set Power under Monoid Homomorphism: $f(s^n) = (f(s))^n$

Informal description

Let $\alpha$ and $\beta$ be monoids, and let $F$ be a type of monoid homomorphisms from $\alpha$ to $\beta$. For any homomorphism $f \in F$, any subset $s \subseteq \alpha$, and any natural number $n$, the image of the $n$-th power of $s$ under $f$ equals the $n$-th power of the image of $s$ under $f$. That is, \[ f(s^n) = (f(s))^n. \]

Set.image_div theorem

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

Full source

@[to_additive]
theorem image_div : m '' (s / t) = m '' s / m '' t :=
  image_image2_distrib <| map_div m

Image of Pointwise Division Equals Pointwise Division of Images

Informal description

For any function $m \colon \alpha \to \beta$ and any subsets $s, t \subseteq \alpha$, the image of the pointwise division set $s / t$ under $m$ equals the pointwise division of the images $m(s)$ and $m(t)$. That is, $$ m(s / t) = m(s) / m(t). $$

Set.div_subset_range theorem

{s t : Set β} (hs : s ⊆ range m) (ht : t ⊆ range m) : s / t ⊆ range m

Full source

@[to_additive]
lemma div_subset_range {s t : Set β} (hs : s ⊆ range m) (ht : t ⊆ range m) : s / t ⊆ range m := by
  rintro _ ⟨a, ha, b, hb, rfl⟩
  obtain ⟨a, rfl⟩ := hs ha
  obtain ⟨b, rfl⟩ := ht hb
  exact ⟨a / b, map_div ..⟩

Range closure under pointwise division: $s / t \subseteq \mathrm{range}(m)$ for $s, t \subseteq \mathrm{range}(m)$

Informal description

Let $m$ be a function from a type $\alpha$ to a type $\beta$. For any subsets $s, t \subseteq \beta$ such that $s \subseteq \mathrm{range}(m)$ and $t \subseteq \mathrm{range}(m)$, the pointwise division set $s / t$ is contained in the range of $m$, i.e., $s / t \subseteq \mathrm{range}(m)$.

Set.preimage_div_preimage_subset theorem

{s t : Set β} : m ⁻¹' s / m ⁻¹' t ⊆ m ⁻¹' (s / t)

Full source

@[to_additive]
theorem preimage_div_preimage_subset {s t : Set β} : m ⁻¹' sm ⁻¹' s / m ⁻¹' t ⊆ m ⁻¹' (s / t) := by
  rintro _ ⟨_, _, _, _, rfl⟩
  exact ⟨_, ‹_›, _, ‹_›, (map_div m ..).symm⟩

Preimage of Division is Subset of Division of Preimages

Informal description

For any function $m \colon \alpha \to \beta$ and any subsets $s, t \subseteq \beta$, the pointwise division of the preimages $m^{-1}(s) / m^{-1}(t)$ is a subset of the preimage of the pointwise division $m^{-1}(s / t)$. In other words, $$ m^{-1}(s) / m^{-1}(t) \subseteq m^{-1}(s / t). $$

Set.preimage_div theorem

 (hm : Injective m) {s t : Set β} (hs : s ⊆ range m) (ht : t ⊆ range m) : m ⁻¹' (s / t) = m ⁻¹' s / m ⁻¹' t

Full source

@[to_additive]
lemma preimage_div (hm : Injective m) {s t : Set β} (hs : s ⊆ range m) (ht : t ⊆ range m) :
    m ⁻¹' (s / t) = m ⁻¹' s / m ⁻¹' t :=
  hm.image_injective <| by
    rw [image_div, image_preimage_eq_iff.2 hs, image_preimage_eq_iff.2 ht,
      image_preimage_eq_iff.2 (div_subset_range m hs ht)]

Preimage of Pointwise Division Equals Pointwise Division of Preimages for Injective Maps

Informal description

Let $m \colon \alpha \to \beta$ be an injective function, and let $s, t \subseteq \beta$ be subsets contained in the range of $m$. Then the preimage of the pointwise division set $s / t$ under $m$ equals the pointwise division of the preimages, i.e., $$ m^{-1}(s / t) = m^{-1}(s) / m^{-1}(t). $$

Set.inv_pi theorem

(s : Set ι) (t : ∀ i, Set (α i)) : (s.pi t)⁻¹ = s.pi fun i ↦ (t i)⁻¹

Full source

@[to_additive (attr := simp)]
lemma inv_pi (s : Set ι) (t : ∀ i, Set (α i)) : (s.pi t)⁻¹ = s.pi fun i ↦ (t i)⁻¹ := by ext x; simp

Inversion of Product Set Equals Product of Inverted Sets

Informal description

For any index set $s \subseteq \iota$ and any family of sets $t_i \subseteq \alpha_i$ (where each $\alpha_i$ has an inversion operation), the pointwise inversion of the product set $\prod_{i \in s} t_i$ is equal to the product set of the pointwise inverses, i.e., $$ \left(\prod_{i \in s} t_i\right)^{-1} = \prod_{i \in s} t_i^{-1}. $$

Set.MapsTo.mul theorem

 [Mul β] {A : Set α} {B₁ B₂ : Set β} {f₁ f₂ : α → β} (h₁ : MapsTo f₁ A B₁) (h₂ : MapsTo f₂ A B₂) :
  MapsTo (f₁ * f₂) A (B₁ * B₂)

Full source

@[to_additive]
lemma MapsTo.mul [Mul β] {A : Set α} {B₁ B₂ : Set β} {f₁ f₂ : α → β}
    (h₁ : MapsTo f₁ A B₁) (h₂ : MapsTo f₂ A B₂) : MapsTo (f₁ * f₂) A (B₁ * B₂) :=
  fun _ h => mul_mem_mul (h₁ h) (h₂ h)

Image of Pointwise Product under Function Multiplication

Informal description

Let $\alpha$ and $\beta$ be types with $\beta$ equipped with a multiplication operation. Given sets $A \subseteq \alpha$, $B_1, B_2 \subseteq \beta$, and functions $f_1, f_2 : \alpha \to \beta$ such that $f_1$ maps $A$ into $B_1$ and $f_2$ maps $A$ into $B_2$, then the pointwise product function $f_1 \cdot f_2$ maps $A$ into the pointwise product set $B_1 \cdot B_2$.

Set.MapsTo.inv theorem

[InvolutiveInv β] {A : Set α} {B : Set β} {f : α → β} (h : MapsTo f A B) : MapsTo (f⁻¹) A (B⁻¹)

Full source

@[to_additive]
lemma MapsTo.inv [InvolutiveInv β] {A : Set α} {B : Set β} {f : α → β} (h : MapsTo f A B) :
    MapsTo (f⁻¹) A (B⁻¹) :=
  fun _ ha => inv_mem_inv.2 (h ha)

Inversion Preserves Set Mapping: $f(A) \subseteq B$ implies $f^{-1}(A) \subseteq B^{-1}$

Informal description

Let $\beta$ be a type with an involutive inversion operation, and let $A \subseteq \alpha$, $B \subseteq \beta$ be sets. If a function $f : \alpha \to \beta$ satisfies $f(A) \subseteq B$, then the inverted function $f^{-1}$ satisfies $f^{-1}(A) \subseteq B^{-1}$, where $B^{-1} = \{x^{-1} \mid x \in B\}$ is the pointwise inverse of $B$.

Set.MapsTo.div theorem

 [Div β] {A : Set α} {B₁ B₂ : Set β} {f₁ f₂ : α → β} (h₁ : MapsTo f₁ A B₁) (h₂ : MapsTo f₂ A B₂) :
  MapsTo (f₁ / f₂) A (B₁ / B₂)

Full source

@[to_additive]
lemma MapsTo.div [Div β] {A : Set α} {B₁ B₂ : Set β} {f₁ f₂ : α → β}
    (h₁ : MapsTo f₁ A B₁) (h₂ : MapsTo f₂ A B₂) : MapsTo (f₁ / f₂) A (B₁ / B₂) :=
  fun _ ha => div_mem_div (h₁ ha) (h₂ ha)

Preservation of Pointwise Division under Function Mapping

Informal description

Let $\alpha$ and $\beta$ be types with a division operation on $\beta$. Given sets $A \subseteq \alpha$, $B_1, B_2 \subseteq \beta$, and functions $f_1, f_2 : \alpha \to \beta$ such that $f_1$ maps $A$ into $B_1$ and $f_2$ maps $A$ into $B_2$, then the pointwise division function $f_1 / f_2$ maps $A$ into the pointwise division set $B_1 / B_2$.

Mathlib.Algebra.Group.Pointwise.Set.Basic

Main declarations

Implementation notes

Tags