Mathlib.Algebra.Group.Pointwise.Finset.Basic

Finset.one definition

: One (Finset α)

Full source

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

Singleton finset containing the multiplicative identity

Informal description

The finset `1 : Finset α` is defined as the singleton set `{1}`, where `1` is the multiplicative identity of the type `α`.

Finset.mem_one theorem

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

Full source

@[to_additive (attr := simp)]
theorem mem_one : a ∈ (1 : Finset α)a ∈ (1 : Finset α) ↔ a = 1 :=
  mem_singleton

Membership in Singleton Finset of Identity: $a \in \{1\} \leftrightarrow a = 1$

Informal description

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

Finset.coe_one theorem

: ↑(1 : Finset α) = (1 : Set α)

Full source

@[to_additive (attr := simp, norm_cast)]
theorem coe_one : ↑(1 : Finset α) = (1 : Set α) :=
  coe_singleton 1

Equality of Singleton Finset and Singleton Set: $\{1\} = \{1\}$

Informal description

The underlying set of the singleton finset $\{1\}$ is equal to the singleton set $\{1\}$ in the type of sets over $\alpha$, where $1$ is the multiplicative identity of $\alpha$.

Finset.coe_eq_one theorem

: (s : Set α) = 1 ↔ s = 1

Full source

@[to_additive (attr := simp, norm_cast)]
lemma coe_eq_one : (s : Set α) = 1 ↔ s = 1 := coe_eq_singleton

Equivalence of Finite Set and Singleton Set $\{1\}$

Informal description

For any finite set $s$ of type $\alpha$, the underlying set of $s$ is equal to the singleton set $\{1\}$ if and only if $s$ is the singleton finite set $\{1\}$.

Finset.one_subset theorem

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

Full source

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

Singleton Subset Criterion: $\{1\} \subseteq s \leftrightarrow 1 \in s$

Informal description

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

Finset.singleton_one theorem

: ({ 1 } : Finset α) = 1

Full source

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

Singleton of One Equals Finset One

Informal description

The singleton finite set containing the multiplicative identity element $1$ of type $\alpha$ is equal to the finset $1$, i.e., $\{1\} = 1$.

Finset.one_mem_one theorem

: (1 : α) ∈ (1 : Finset α)

Full source

@[to_additive]
theorem one_mem_one : (1 : α) ∈ (1 : Finset α) :=
  mem_singleton_self _

$1 \in \{1\}$ in finsets

Informal description

The multiplicative identity element $1$ of type $\alpha$ is an element of the singleton finset $\{1\}$.

Finset.one_nonempty theorem

: (1 : Finset α).Nonempty

Full source

@[to_additive (attr := simp, aesop safe apply (rule_sets := [finsetNonempty]))]
theorem one_nonempty : (1 : Finset α).Nonempty :=
  ⟨1, one_mem_one⟩

Nonemptiness of Singleton Finset $\{1\}$

Informal description

The singleton finset $\{1\}$ is nonempty, where $1$ is the multiplicative identity of the type $\alpha$.

Finset.map_one theorem

{f : α ↪ β} : map f 1 = {f 1}

Full source

@[to_additive (attr := simp)]
protected theorem map_one {f : α ↪ β} : map f 1 = {f 1} :=
  map_singleton f 1

Image of Singleton One Finset under Injective Map: $f(\{1\}) = \{f(1)\}$

Informal description

For any injective function embedding $f \colon \alpha \hookrightarrow \beta$, the image of the singleton finset $\{1\}$ under $f$ is the singleton finset $\{f(1)\}$.

Finset.image_one theorem

[DecidableEq β] {f : α → β} : image f 1 = {f 1}

Full source

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

Image of Singleton One Finset is Singleton of Image

Informal description

For any function $f : \alpha \to \beta$ (with decidable equality on $\beta$), the image of the singleton finset $\{1\}$ under $f$ is the singleton finset $\{f(1)\}$.

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

Characterization of Subsets of Singleton One: $s \subseteq \{1\} \leftrightarrow s = \emptyset \lor s = \{1\}$

Informal description

For any finite set $s$ of type $\alpha$, $s$ is a subset of the singleton set $\{1\}$ if and only if $s$ is either the empty set or the singleton set $\{1\}$ itself. In other words, $s \subseteq \{1\} \leftrightarrow s = \emptyset \lor s = \{1\}$.

Finset.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 One Characterization: $s \subseteq \{1\} \leftrightarrow s = \{1\}$

Informal description

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

Finset.card_one theorem

: #(1 : Finset α) = 1

Full source

@[to_additive (attr := simp)]
theorem card_one : #(1 : Finset α) = 1 :=
  card_singleton _

Cardinality of Singleton Finset Containing One: $\#\{1\} = 1$

Informal description

The cardinality of the singleton finset $\{1\}$ is $1$, i.e., $\#\{1\} = 1$.

Finset.singletonOneHom definition

: OneHom α (Finset α)

Full source

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

Singleton construction as an identity-preserving homomorphism

Informal description

The function that maps an element $a$ of type $\alpha$ to the singleton finite set $\{a\}$ is an identity-preserving homomorphism, i.e., it satisfies $\text{singletonOneHom}(1) = \{1\}$.

Finset.coe_singletonOneHom theorem

: (singletonOneHom : α → Finset α) = singleton

Full source

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

Equality of Singleton Construction and Identity-Preserving Homomorphism on Finite Sets

Informal description

The function `singletonOneHom` from a type $\alpha$ to the type of finite subsets of $\alpha$ is equal to the singleton construction function, i.e., for any $a \in \alpha$, `singletonOneHom(a) = {a}`.

Finset.singletonOneHom_apply theorem

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

Full source

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

Singleton Construction Homomorphism Application: $\text{singletonOneHom}(a) = \{a\}$

Informal description

For any element $a$ of type $\alpha$, the application of the singleton construction homomorphism to $a$ yields the singleton finite set $\{a\}$.

Finset.imageOneHom definition

[DecidableEq β] [One β] [FunLike F α β] [OneHomClass F α β] (f : F) : OneHom (Finset α) (Finset β)

Full source

/-- Lift a `OneHom` to `Finset` via `image`. -/
@[to_additive (attr := simps) "Lift a `ZeroHom` to `Finset` via `image`"]
def imageOneHom [DecidableEq β] [One β] [FunLike F α β] [OneHomClass F α β] (f : F) :
    OneHom (Finset α) (Finset β) where
  toFun := Finset.image f
  map_one' := by rw [image_one, map_one, singleton_one]

Lifting of identity-preserving homomorphism to finite sets

Informal description

Given a type $\beta$ with decidable equality and a multiplicative identity, and a type $\alpha$ with a multiplicative identity, the function `imageOneHom` lifts a `OneHom` (an identity-preserving homomorphism) $f : \alpha \to \beta$ to a `OneHom` between the finsets of $\alpha$ and $\beta$. Specifically, it maps a finite set $s \subseteq \alpha$ to the finite set $\{f(x) \mid x \in s\} \subseteq \beta$, and preserves the multiplicative identity by mapping $\{1_\alpha\}$ to $\{1_\beta\}$.

Finset.sup_one theorem

[SemilatticeSup β] [OrderBot β] (f : α → β) : sup 1 f = f 1

Full source

@[to_additive (attr := simp)]
lemma sup_one [SemilatticeSup β] [OrderBot β] (f : α → β) : sup 1 f = f 1 := sup_singleton

Supremum over Singleton $\{1\}$ Equals $f(1)$

Informal description

Let $\beta$ be a join-semilattice with a least element $\bot$, and let $f : \alpha \to \beta$ be a function. Then the supremum of $f$ over the singleton finset $\{1\}$ is equal to $f(1)$, i.e., \[ \sup_{\{1\}} f = f(1). \]

Finset.sup'_one theorem

[SemilatticeSup β] (f : α → β) : sup' 1 one_nonempty f = f 1

Full source

@[to_additive (attr := simp)]
lemma sup'_one [SemilatticeSup β] (f : α → β) : sup' 1 one_nonempty f = f 1 := rfl

Supremum over Singleton $\{1\}$ Equals $f(1)$

Informal description

For any join-semilattice $\beta$ and any function $f \colon \alpha \to \beta$, the supremum of $f$ over the singleton finset $\{1\}$ is equal to $f(1)$, i.e., \[ \sup_{\{1\}} f = f(1). \]

Finset.inf_one theorem

[SemilatticeInf β] [OrderTop β] (f : α → β) : inf 1 f = f 1

Full source

@[to_additive (attr := simp)]
lemma inf_one [SemilatticeInf β] [OrderTop β] (f : α → β) : inf 1 f = f 1 := inf_singleton

Infimum over Singleton $\{1\}$ Equals $f(1)$

Informal description

For any meet-semilattice $\beta$ with a top element $\top$ and any function $f \colon \alpha \to \beta$, the infimum of $f$ over the singleton finset $\{1\}$ is equal to $f(1)$, i.e., \[ \inf_{\{1\}} f = f(1). \]

Finset.inf'_one theorem

[SemilatticeInf β] (f : α → β) : inf' 1 one_nonempty f = f 1

Full source

@[to_additive (attr := simp)]
lemma inf'_one [SemilatticeInf β] (f : α → β) : inf' 1 one_nonempty f = f 1 := rfl

Infimum over Singleton $\{1\}$ Equals $f(1)$ in a Meet-Semilattice

Informal description

For any meet-semilattice $\beta$ and any function $f \colon \alpha \to \beta$, the infimum of $f$ over the nonempty singleton finset $\{1\}$ is equal to $f(1)$, i.e., \[ \inf'_{\{1\}} f = f(1). \]

Finset.max_one theorem

[LinearOrder α] : (1 : Finset α).max = 1

Full source

@[to_additive (attr := simp)]
lemma max_one [LinearOrder α] : (1 : Finset α).max = 1 := rfl

Maximum of Singleton Finset $\{1\}$ is $1$ in a Linear Order

Informal description

For any linearly ordered type $\alpha$, the maximum element of the singleton finset $\{1\}$ is $1$.

Finset.min_one theorem

[LinearOrder α] : (1 : Finset α).min = 1

Full source

@[to_additive (attr := simp)]
lemma min_one [LinearOrder α] : (1 : Finset α).min = 1 := rfl

Minimum of Singleton Finset $\{1\}$ is $1$ in a Linear Order

Informal description

For any linearly ordered type $\alpha$, the minimum element of the singleton finset $\{1\}$ is $1$.

Finset.max'_one theorem

[LinearOrder α] : (1 : Finset α).max' one_nonempty = 1

Full source

@[to_additive (attr := simp)]
lemma max'_one [LinearOrder α] : (1 : Finset α).max' one_nonempty = 1 := rfl

Maximum of Singleton $\{1\}$ in Linear Order

Informal description

For any linearly ordered type $\alpha$, the maximum element of the singleton finset $\{1\}$ is $1$, where the nonemptiness of $\{1\}$ is given by `one_nonempty`.

Finset.min'_one theorem

[LinearOrder α] : (1 : Finset α).min' one_nonempty = 1

Full source

@[to_additive (attr := simp)]
lemma min'_one [LinearOrder α] : (1 : Finset α).min' one_nonempty = 1 := rfl

Minimum of Singleton $\{1\}$ is $1$ in a Linear Order

Informal description

For any linearly ordered type $\alpha$, the minimum element of the singleton finset $\{1\}$ is $1$, where $1$ is the multiplicative identity of $\alpha$.

Finset.image_op_one theorem

[DecidableEq α] : (1 : Finset α).image op = 1

Full source

@[to_additive (attr := simp)]
lemma image_op_one [DecidableEq α] : (1 : Finset α).image op = 1 := rfl

Preservation of Identity under Opposite Mapping in Finite Sets

Informal description

For any type $\alpha$ with decidable equality, the image of the singleton finset $\{1\}$ under the canonical embedding into the multiplicative opposite $\alpha^\text{op}$ is equal to the singleton finset $\{1\}$ in $\alpha^\text{op}$.

Finset.map_op_one theorem

: (1 : Finset α).map opEquiv.toEmbedding = 1

Full source

@[to_additive (attr := simp)]
lemma map_op_one : (1 : Finset α).map opEquiv.toEmbedding = 1 := rfl

Preservation of Multiplicative Identity under Opposite Mapping

Informal description

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

Finset.one_product_one theorem

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

Full source

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

Cartesian product of singleton identities equals product identity

Informal description

For any type $\alpha$ with a multiplicative identity and any type $\beta$ with a multiplicative identity, the Cartesian product of the singleton sets $\{1_\alpha\}$ and $\{1_\beta\}$ is equal to the singleton set $\{1_{\alpha \times \beta}\}$, where $1_{\alpha \times \beta} = (1_\alpha, 1_\beta)$ is the multiplicative identity in the product type $\alpha \times \beta$.

Finset.inv definition

: Inv (Finset α)

Full source

/-- The pointwise inversion of finset `s⁻¹` is defined as `{x⁻¹ | x ∈ s}` in locale `Pointwise`. -/
@[to_additive
      "The pointwise negation of finset `-s` is defined as `{-x | x ∈ s}` in locale `Pointwise`."]
protected def inv : Inv (Finset α) :=
  ⟨image Inv.inv⟩

Pointwise inversion of a finite set

Informal description

The pointwise inversion operation on a finite set $s$ of elements with inverses is defined as the finite set $\{x^{-1} \mid x \in s\}$.

Finset.inv_def theorem

: s⁻¹ = s.image fun x => x⁻¹

Full source

@[to_additive]
theorem inv_def : s⁻¹ = s.image fun x => x⁻¹ :=
  rfl

Definition of Pointwise Inverse for Finite Sets via Image

Informal description

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

Finset.image_inv_eq_inv theorem

(s : Finset α) : s.image (·⁻¹) = s⁻¹

Full source

@[to_additive] lemma image_inv_eq_inv (s : Finset α) : s.image (·⁻¹) = s⁻¹ := rfl

Image of Inversion Equals Pointwise Inverse for Finite Sets

Informal description

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

Finset.mem_inv theorem

{x : α} : x ∈ s⁻¹ ↔ ∃ y ∈ s, y⁻¹ = x

Full source

@[to_additive]
theorem mem_inv {x : α} : x ∈ s⁻¹x ∈ s⁻¹ ↔ ∃ y ∈ s, y⁻¹ = x :=
  mem_image

Characterization of Membership in Pointwise Inverse of Finite Set

Informal description

For any element $x$ of type $\alpha$ and any finite set $s \subseteq \alpha$, $x$ belongs to the pointwise inverse $s^{-1}$ if and only if there exists an element $y \in s$ such that $y^{-1} = x$.

Finset.inv_mem_inv theorem

(ha : a ∈ s) : a⁻¹ ∈ s⁻¹

Full source

@[to_additive]
theorem inv_mem_inv (ha : a ∈ s) : a⁻¹a⁻¹ ∈ s⁻¹ :=
  mem_image_of_mem _ ha

Inverse of Element in Finite Set is in Pointwise Inverse

Informal description

For any element $a$ in a finite set $s$ of a type $\alpha$ with an inversion operation, the inverse $a^{-1}$ belongs to the pointwise inverse set $s^{-1}$.

Finset.card_inv_le theorem

: #s⁻¹ ≤ #s

Full source

@[to_additive]
theorem card_inv_le : #s⁻¹ ≤ #s :=
  card_image_le

Cardinality Inequality for Pointwise Inversion: $\#(s^{-1}) \leq \#s$

Informal description

For any finite set $s$ of elements with inverses, the cardinality of the pointwise inverse set $s^{-1} = \{x^{-1} \mid x \in s\}$ is less than or equal to the cardinality of $s$, i.e., $\#(s^{-1}) \leq \#s$.

Finset.inv_empty theorem

: (∅ : Finset α)⁻¹ = ∅

Full source

@[to_additive (attr := simp)]
theorem inv_empty : (∅ : Finset α)⁻¹ = ∅ :=
  image_empty _

Pointwise Inverse of Empty Set is Empty

Informal description

The pointwise inverse of the empty finite set is the empty set, i.e., $\emptyset^{-1} = \emptyset$.

Finset.inv_nonempty_iff theorem

: s⁻¹.Nonempty ↔ s.Nonempty

Full source

@[to_additive (attr := simp)]
theorem inv_nonempty_iff : s⁻¹s⁻¹.Nonempty ↔ s.Nonempty := image_nonempty

Nonempty Inversion Criterion for Finite Sets

Informal description

For any finite set $s$ of elements with inverses, the pointwise inverse $s^{-1} = \{x^{-1} \mid x \in s\}$ is nonempty if and only if $s$ is nonempty. In symbols: $$ s^{-1} \neq \emptyset \leftrightarrow s \neq \emptyset $$

Finset.inv_eq_empty theorem

: s⁻¹ = ∅ ↔ s = ∅

Full source

@[to_additive (attr := simp)]
theorem inv_eq_empty : s⁻¹s⁻¹ = ∅ ↔ s = ∅ := image_eq_empty

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

Informal description

For any finite set $s$ of elements with inverses, the pointwise inverse of $s$ is empty if and only if $s$ is empty. In symbols: $$ s^{-1} = \emptyset \leftrightarrow s = \emptyset $$

Finset.inv_subset_inv theorem

(h : s ⊆ t) : s⁻¹ ⊆ t⁻¹

Full source

@[to_additive (attr := mono, gcongr)]
theorem inv_subset_inv (h : s ⊆ t) : s⁻¹s⁻¹ ⊆ t⁻¹ :=
  image_subset_image h

Inversion Preserves Subset Relation for Finite Sets

Informal description

For any two finite sets $s$ and $t$ of elements with inverses, if $s$ is a subset of $t$, then the pointwise inverse of $s$ is a subset of the pointwise inverse of $t$, i.e., $s \subseteq t$ implies $s^{-1} \subseteq t^{-1}$.

Finset.inv_singleton theorem

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

Full source

@[to_additive (attr := simp)]
theorem inv_singleton (a : α) : ({a} : Finset α)⁻¹ = {a⁻¹} :=
  image_singleton _ _

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

Informal description

For any element $a$ of a type $\alpha$ with an inversion operation, the pointwise inverse of the singleton finite set $\{a\}$ is the singleton set $\{a^{-1}\}$.

Finset.inv_insert theorem

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

Full source

@[to_additive (attr := simp)]
theorem inv_insert (a : α) (s : Finset α) : (insert a s)⁻¹ = insert a⁻¹ s⁻¹ :=
  image_insert _ _ _

Pointwise Inverse of Inserted Element: $(\{a\} \cup s)^{-1} = \{a^{-1}\} \cup s^{-1}$

Informal description

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

Finset.sup_inv theorem

[SemilatticeSup β] [OrderBot β] (s : Finset α) (f : α → β) : sup s⁻¹ f = sup s (f ·⁻¹)

Full source

@[to_additive (attr := simp)]
lemma sup_inv [SemilatticeSup β] [OrderBot β] (s : Finset α) (f : α → β) :
    sup s⁻¹ f = sup s (f ·⁻¹) :=
  sup_image ..

Supremum over Pointwise Inverse Set Equals Supremum of Inverted Function

Informal description

Let $\alpha$ be a type with an inversion operation and $\beta$ be a join-semilattice with a bottom element $\bot$. For any finite set $s \subseteq \alpha$ and any function $f : \alpha \to \beta$, the supremum of $f$ over the pointwise inverse set $s^{-1} = \{x^{-1} \mid x \in s\}$ is equal to the supremum of the function $x \mapsto f(x^{-1})$ over $s$. That is, \[ \sup_{y \in s^{-1}} f(y) = \sup_{x \in s} f(x^{-1}). \]

Finset.sup'_inv theorem

 [SemilatticeSup β] {s : Finset α} (hs : s⁻¹.Nonempty) (f : α → β) : sup' s⁻¹ hs f = sup' s hs.of_inv (f ·⁻¹)

Full source

@[to_additive (attr := simp)]
lemma sup'_inv [SemilatticeSup β] {s : Finset α} (hs : s⁻¹.Nonempty) (f : α → β) :
    sup' s⁻¹ hs f = sup' s hs.of_inv (f ·⁻¹) :=
  sup'_image ..

Supremum over Inverse Set Equals Supremum of Inverted Function for Nonempty Finite Sets

Informal description

Let $\alpha$ be a type with an inversion operation and $\beta$ be a join-semilattice. For any finite set $s \subseteq \alpha$ such that the pointwise inverse set $s^{-1} = \{x^{-1} \mid x \in s\}$ is nonempty, and for any function $f : \alpha \to \beta$, the supremum of $f$ over $s^{-1}$ equals the supremum of the function $x \mapsto f(x^{-1})$ over $s$. That is, \[ \sup'_{y \in s^{-1}} f(y) = \sup'_{x \in s} f(x^{-1}), \] where $\sup'$ denotes the supremum operation for nonempty finite sets.

Finset.inf_inv theorem

[SemilatticeInf β] [OrderTop β] (s : Finset α) (f : α → β) : inf s⁻¹ f = inf s (f ·⁻¹)

Full source

@[to_additive (attr := simp)]
lemma inf_inv [SemilatticeInf β] [OrderTop β] (s : Finset α) (f : α → β) :
    inf s⁻¹ f = inf s (f ·⁻¹) :=
  inf_image ..

Infimum over Pointwise Inverse Set Equals Infimum of Inverted Function

Informal description

Let $\alpha$ be a type with an inversion operation and $\beta$ be a meet-semilattice with a top element $\top$. For any finite set $s \subseteq \alpha$ and any function $f \colon \alpha \to \beta$, the infimum of $f$ over the pointwise inverse set $s^{-1} = \{x^{-1} \mid x \in s\}$ is equal to the infimum of the function $x \mapsto f(x^{-1})$ over $s$. That is, \[ \inf_{y \in s^{-1}} f(y) = \inf_{x \in s} f(x^{-1}). \]

Finset.inf'_inv theorem

 [SemilatticeInf β] {s : Finset α} (hs : s⁻¹.Nonempty) (f : α → β) : inf' s⁻¹ hs f = inf' s hs.of_inv (f ·⁻¹)

Full source

@[to_additive (attr := simp)]
lemma inf'_inv [SemilatticeInf β] {s : Finset α} (hs : s⁻¹.Nonempty) (f : α → β) :
    inf' s⁻¹ hs f = inf' s hs.of_inv (f ·⁻¹) :=
  inf'_image ..

Infimum over Inverse Set Equals Infimum of Inverted Function for Nonempty Finite Sets

Informal description

Let $\alpha$ be a type with an inversion operation and $\beta$ be a meet-semilattice. For any finite set $s \subseteq \alpha$ such that the pointwise inverse set $s^{-1} = \{x^{-1} \mid x \in s\}$ is nonempty, and for any function $f \colon \alpha \to \beta$, the infimum of $f$ over $s^{-1}$ equals the infimum of the function $x \mapsto f(x^{-1})$ over $s$. That is, \[ \inf'_{y \in s^{-1}} f(y) = \inf'_{x \in s} f(x^{-1}), \] where $\inf'$ denotes the infimum operation for nonempty finite sets.

Finset.image_op_inv theorem

(s : Finset α) : s⁻¹.image op = (s.image op)⁻¹

Full source

@[to_additive] lemma image_op_inv (s : Finset α) : s⁻¹.image op = (s.image op)⁻¹ :=
  image_comm op_inv

Image of Pointwise Inverse under Opposite Embedding Equals Pointwise Inverse of Image

Informal description

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

Finset.map_op_inv theorem

(s : Finset α) : s⁻¹.map opEquiv.toEmbedding = (s.map opEquiv.toEmbedding)⁻¹

Full source

@[to_additive]
lemma map_op_inv (s : Finset α) : s⁻¹.map opEquiv.toEmbedding = (s.map opEquiv.toEmbedding)⁻¹ := by
  simp [map_eq_image, image_op_inv]

Image of Pointwise Inverse under Opposite Embedding Equals Pointwise Inverse of Image

Informal description

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

Finset.mem_inv' theorem

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

Full source

@[to_additive (attr := simp)]
lemma mem_inv' : a ∈ s⁻¹a ∈ s⁻¹ ↔ a⁻¹ ∈ s := by simp [mem_inv, inv_eq_iff_eq_inv]

Membership in Pointwise Inverse of Finite Set

Informal description

For any element $a$ of type $\alpha$ and any finite subset $s$ of $\alpha$, the element $a$ belongs to the pointwise inverse $s^{-1}$ if and only if the inverse of $a$ belongs to $s$. In other words, $a \in s^{-1} \leftrightarrow a^{-1} \in s$.

Finset.coe_inv theorem

(s : Finset α) : ↑s⁻¹ = (s : Set α)⁻¹

Full source

@[to_additive (attr := simp, norm_cast)]
theorem coe_inv (s : Finset α) : ↑s⁻¹ = (s : Set α)⁻¹ := coe_image.trans Set.image_inv_eq_inv

Coercion of Pointwise Inverse of Finite Set Equals Pointwise Inverse of Coerced Set: $\overline{s^{-1}} = (\overline{s})^{-1}$

Informal description

For any finite set $s$ of elements in a type $\alpha$ equipped with an inversion operation, the coercion of the pointwise inverse set $s^{-1}$ to a set equals the pointwise inverse of the set obtained by coercing $s$. That is, $\overline{s^{-1}} = (\overline{s})^{-1}$, where $\overline{\cdot}$ denotes the coercion from finite sets to sets and $(\cdot)^{-1}$ denotes the pointwise inversion operation.

Finset.card_inv theorem

(s : Finset α) : #s⁻¹ = #s

Full source

@[to_additive (attr := simp)]
theorem card_inv (s : Finset α) : #s⁻¹ = #s := card_image_of_injective _ inv_injective

Cardinality Preservation under Pointwise Inversion: $|s^{-1}| = |s|$

Informal description

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

Finset.preimage_inv theorem

(s : Finset α) : s.preimage (·⁻¹) inv_injective.injOn = s⁻¹

Full source

@[to_additive (attr := simp)]
theorem preimage_inv (s : Finset α) : s.preimage (·⁻¹) inv_injective.injOn = s⁻¹ :=
  coe_injective <| by rw [coe_preimage, Set.inv_preimage, coe_inv]

Preimage under Inversion Equals Pointwise Inverse: $\text{preimage}(s, (\cdot)^{-1}) = s^{-1}$

Informal description

For any finite set $s$ of elements in a type $\alpha$ equipped with an involutive inversion operation, the preimage of $s$ under the inversion map $x \mapsto x^{-1}$ is equal to the pointwise inverse set $s^{-1} = \{x^{-1} \mid x \in s\}$.

Finset.inv_univ theorem

[Fintype α] : (univ : Finset α)⁻¹ = univ

Full source

@[to_additive (attr := simp)]
lemma inv_univ [Fintype α] : (univ : Finset α)⁻¹ = univ := by ext; simp

Inversion of Universal Finite Set Equals Itself

Informal description

For a finite type $\alpha$ with an involutive inversion operation, the pointwise inversion of the universal finite set (containing all elements of $\alpha$) is equal to itself, i.e., $\text{univ}^{-1} = \text{univ}$.

Finset.inv_inter theorem

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

Full source

@[to_additive (attr := simp)]
lemma inv_inter (s t : Finset α) : (s ∩ t)⁻¹ = s⁻¹s⁻¹ ∩ t⁻¹ := coe_injective <| by simp

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

Informal description

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

Finset.inv_product theorem

[DecidableEq β] [InvolutiveInv β] (s : Finset α) (t : Finset β) : (s ×ˢ t)⁻¹ = s⁻¹ ×ˢ t⁻¹

Full source

@[to_additive (attr := simp)]
lemma inv_product [DecidableEq β] [InvolutiveInv β] (s : Finset α) (t : Finset β) :
    (s ×ˢ t)⁻¹ = s⁻¹ ×ˢ t⁻¹ := mod_cast s.toSet.inv_prod t.toSet

Inversion of Cartesian Product of Finite Sets

Informal description

Let $\alpha$ and $\beta$ be types with $\beta$ equipped with an involutive inversion operation (i.e., $(x^{-1})^{-1} = x$ for all $x \in \beta$). For any finite sets $s \subseteq \alpha$ and $t \subseteq \beta$, the pointwise inversion of their Cartesian product equals the Cartesian product of their pointwise inversions, i.e., $(s \times t)^{-1} = s^{-1} \times t^{-1}$.

Finset.mul definition

: Mul (Finset α)

Full source

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

Pointwise multiplication of finite sets

Informal description

The pointwise multiplication operation on finite sets, where for finite sets $ s $ and $ t $ of type $ \alpha $, the product $ s * t $ is defined as the finite set consisting of all elements $ x * y $ with $ x \in s $ and $ y \in t $. This operation is defined in the locale `Pointwise`.

Finset.mul_def theorem

: s * t = (s ×ˢ t).image fun p : α × α => p.1 * p.2

Full source

@[to_additive]
theorem mul_def : s * t = (s ×ˢ t).image fun p : α × α => p.1 * p.2 :=
  rfl

Definition of Pointwise Multiplication for Finite Sets via Cartesian Product

Informal description

For any finite sets $s$ and $t$ of elements of type $\alpha$, the pointwise multiplication $s * t$ is equal to the image of the Cartesian product $s \times t$ under the multiplication function $(x, y) \mapsto x * y$.

Finset.image_mul_product theorem

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

Full source

@[to_additive]
theorem image_mul_product : ((s ×ˢ t).image fun x : α × α => x.fst * x.snd) = s * t :=
  rfl

Image of Cartesian Product under Multiplication Equals Pointwise Product of Finite Sets

Informal description

For finite sets $s$ and $t$ of a type $\alpha$ equipped with multiplication, the image of the Cartesian product $s \times t$ under the multiplication function $(x,y) \mapsto x * y$ is equal to the pointwise product $s * t$ of the sets.

Finset.mem_mul theorem

{x : α} : x ∈ s * t ↔ ∃ y ∈ s, ∃ z ∈ t, y * z = x

Full source

@[to_additive]
theorem mem_mul {x : α} : x ∈ s * tx ∈ s * t ↔ ∃ y ∈ s, ∃ z ∈ t, y * z = x := mem_image₂

Membership Criterion for Pointwise Product of Finite Sets

Informal description

For any element $x$ of type $\alpha$, $x$ belongs to the pointwise product of finite sets $s$ and $t$ if and only if there exist elements $y \in s$ and $z \in t$ such that $y * z = x$.

Finset.coe_mul theorem

(s t : Finset α) : (↑(s * t) : Set α) = ↑s * ↑t

Full source

@[to_additive (attr := simp, norm_cast)]
theorem coe_mul (s t : Finset α) : (↑(s * t) : Set α) = ↑s * ↑t :=
  coe_image₂ _ _ _

Equality of Pointwise Products: $\overline{s * t} = \overline{s} * \overline{t}$

Informal description

For any finite sets $s$ and $t$ of a type $\alpha$ equipped with multiplication, the underlying set of the pointwise product $s * t$ is equal to the pointwise product of the underlying sets of $s$ and $t$. That is, $\overline{s * t} = \overline{s} * \overline{t}$, where $\overline{\cdot}$ denotes the underlying set of a finite set.

Finset.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_image₂_of_mem

Closure of Finite Set Multiplication under Pointwise Product

Informal description

For any elements $a \in s$ and $b \in t$ in finite sets $s$ and $t$ of a type $\alpha$ with multiplication, the product $a * b$ belongs to the pointwise product set $s * t$.

Finset.card_mul_le theorem

: #(s * t) ≤ #s * #t

Full source

@[to_additive]
theorem card_mul_le : #(s * t) ≤ #s * #t :=
  card_image₂_le _ _ _

Cardinality Bound for Pointwise Product of Finite Sets: $|s \cdot t| \leq |s| \cdot |t|$

Informal description

For any two finite sets $s$ and $t$ in a type $\alpha$ equipped with a multiplication operation, the cardinality of their pointwise product set $s \cdot t$ is less than or equal to the product of their cardinalities, i.e., \[ |s \cdot t| \leq |s| \cdot |t|. \]

Finset.card_mul_iff theorem

: #(s * t) = #s * #t ↔ (s ×ˢ t : Set (α × α)).InjOn fun p => p.1 * p.2

Full source

@[to_additive]
theorem card_mul_iff :
    #(s * t)#(s * t) = #s * #t ↔ (s ×ˢ t : Set (α × α)).InjOn fun p => p.1 * p.2 :=
  card_image₂_iff

Cardinality Condition for Pointwise Product of Finite Sets: $|s * t| = |s||t| \iff$ Multiplication is Injective on $s \times t$

Informal description

For finite sets $s$ and $t$ in a type $\alpha$ with multiplication, the cardinality of their pointwise product $s * t$ equals the product of their cardinalities if and only if the multiplication function $(x,y) \mapsto x * y$ is injective on the Cartesian product set $s \times t$. That is, \[ |s * t| = |s| \cdot |t| \iff \text{the map } (x,y) \mapsto x * y \text{ is injective on } s \times t. \]

Finset.empty_mul theorem

(s : Finset α) : ∅ * s = ∅

Full source

@[to_additive (attr := simp)]
theorem empty_mul (s : Finset α) : ∅ * s = ∅ :=
  image₂_empty_left

Empty Set is Left Annihilator for Pointwise Multiplication of Finite Sets

Informal description

For any finite set $s$ of type $\alpha$, the pointwise product of the empty set with $s$ is the empty set, i.e., $\emptyset * s = \emptyset$.

Finset.mul_empty theorem

(s : Finset α) : s * ∅ = ∅

Full source

@[to_additive (attr := simp)]
theorem mul_empty (s : Finset α) : s * ∅ = ∅ :=
  image₂_empty_right

Pointwise multiplication with empty set yields empty set

Informal description

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

Finset.mul_eq_empty theorem

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

Full source

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

Empty Product Criterion for Finite Sets

Informal description

For any two finite sets $s$ and $t$ in a type $\alpha$ with a multiplication operation, the pointwise product $s * 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 $$

Finset.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 :=
  image₂_nonempty_iff

Nonempty Criterion for Pointwise Product of Finite Sets

Informal description

For any two finite sets $s$ and $t$ in a type $\alpha$ with a multiplication operation, the pointwise product $s * t$ is nonempty if and only if both $s$ and $t$ are nonempty. That is: $$ s * t \neq \emptyset \leftrightarrow s \neq \emptyset \land t \neq \emptyset $$

Finset.Nonempty.mul theorem

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

Full source

@[to_additive (attr := aesop safe apply (rule_sets := [finsetNonempty]))]
theorem Nonempty.mul : s.Nonempty → t.Nonempty → (s * t).Nonempty :=
  Nonempty.image₂

Nonempty Product of Nonempty Finite Sets

Informal description

For any two nonempty finite sets $s$ and $t$ in a type $\alpha$ with a multiplication operation, their pointwise product $s * t$ is also nonempty.

Finset.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_image₂_left

Nonemptiness of Left Factor in Nonempty Pointwise Product of Finite Sets

Informal description

For any finite sets $s$ and $t$ in a type $\alpha$ with a multiplication operation, if the pointwise product $s * t$ is nonempty, then $s$ is nonempty.

Finset.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_image₂_right

Nonemptiness of Right Factor in Pointwise Product of Finite Sets

Informal description

For any finite sets $s$ and $t$ in a type $\alpha$ with a multiplication operation, if the pointwise product $s * t$ is nonempty, then $t$ is nonempty.

Finset.singleton_mul_singleton theorem

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

Full source

@[to_additive (attr := simp)]
theorem singleton_mul_singleton (a b : α) : ({a} : Finset α) * {b} = {a * b} :=
  image₂_singleton

Pointwise product of singletons: $\{a\} * \{b\} = \{a * b\}$

Informal description

For any elements $a$ and $b$ in a type $\alpha$ with a multiplication operation, the pointwise product of the singleton sets $\{a\}$ and $\{b\}$ is the singleton set $\{a * b\}$.

Finset.mul_subset_mul theorem

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

Full source

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

Monotonicity of Pointwise Multiplication under Subset Inclusion

Informal description

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

Finset.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₂ :=
  image₂_subset_left

Left Monotonicity of Pointwise Multiplication under Right Subset Inclusion

Informal description

For any finite sets $s, t_1, t_2$ in a type $\alpha$ with a multiplication operation, if $t_1 \subseteq t_2$, then the pointwise product $s * t_1$ is a subset of $s * t_2$.

Finset.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 :=
  image₂_subset_right

Right Monotonicity of Pointwise Multiplication for Finite Sets

Informal description

For any finite sets $s_1, s_2, t$ in a type $\alpha$ with a multiplication operation, if $s_1 \subseteq s_2$, then the pointwise product $s_1 * t$ is a subset of the pointwise product $s_2 * t$.

Finset.instMulLeftMono instance

: MulLeftMono (Finset α)

Full source

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

Left Monotonicity of Pointwise Multiplication on Finite Sets

Informal description

For any type $\alpha$ with a multiplication operation, the pointwise multiplication operation on finite subsets of $\alpha$ is left monotone with respect to the subset relation. That is, for any finite sets $s, t_1, t_2 \subseteq \alpha$, if $t_1 \subseteq t_2$, then $s * t_1 \subseteq s * t_2$.

Finset.instMulRightMono instance

: MulRightMono (Finset α)

Full source

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

Right-Monotonicity of Pointwise Multiplication on Finite Sets

Informal description

For any type $\alpha$ with a multiplication operation and a partial order, the pointwise multiplication operation on finite subsets of $\alpha$ is right-monotone. That is, for any finite sets $s_1, s_2, t \subseteq \alpha$, if $s_1 \subseteq s_2$, then $s_1 * t \subseteq s_2 * t$.

Finset.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 :=
  image₂_subset_iff

Subset Criterion for Pointwise Product of Finite Sets: $s * t \subseteq u \leftrightarrow \forall x \in s, \forall y \in t, x * y \in u$

Informal description

For finite sets $s$, $t$, and $u$ in a type $\alpha$ with a multiplication operation, the pointwise product $s * t$ is a subset of $u$ if and only if for every $x \in s$ and $y \in t$, the product $x * y$ belongs to $u$.

Finset.union_mul theorem

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

Full source

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

Distributivity of Pointwise Multiplication over Union: $(s_1 \cup s_2) * t = s_1 * t \cup s_2 * t$

Informal description

For any finite sets $s_1, s_2, t$ in a type $\alpha$ 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 * t$ and $s_2 * t$. That is, $$(s_1 \cup s_2) * t = (s_1 * t) \cup (s_2 * t).$$

Finset.mul_union theorem

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

Full source

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

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

Informal description

For any finite sets $s$, $t_1$, and $t_2$ of a type $\alpha$ with a multiplication operation, the pointwise multiplication of $s$ with the union $t_1 \cup t_2$ is equal to the union of the pointwise multiplications $s * t_1$ and $s * t_2$. That is, \[ s * (t_1 \cup t_2) = (s * t_1) \cup (s * t_2). \]

Finset.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) :=
  image₂_inter_subset_left

Subset Property of Pointwise Multiplication over Intersection: $(s_1 \cap s_2) * t \subseteq (s_1 * t) \cap (s_2 * t)$

Informal description

For any finite sets $s_1, s_2, t$ in a type $\alpha$ 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 * t$ and $s_2 * t$. That is, $$(s_1 \cap s_2) * t \subseteq (s_1 * t) \cap (s_2 * t).$$

Finset.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₂) :=
  image₂_inter_subset_right

Subset Property of Pointwise Multiplication over Intersection in Second Argument: $s * (t_1 \cap t_2) \subseteq s * t_1 \cap s * t_2$

Informal description

For any finite sets $s$, $t_1$, and $t_2$ of a type $\alpha$ with a multiplication operation, the pointwise multiplication of $s$ with the intersection $t_1 \cap t_2$ is a subset of the intersection of the pointwise multiplications $s * t_1$ and $s * t_2$. That is, \[ s * (t_1 \cap t_2) \subseteq (s * t_1) \cap (s * t_2). \]

Finset.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₂ :=
  image₂_inter_union_subset_union

Subset Property for Pointwise Multiplication of Intersection and Union of Finite Sets

Informal description

For any finite sets $s₁, s₂, t₁, t₂$ of a type $\alpha$ with a multiplication operation, the pointwise product of the intersection $s₁ \cap s₂$ with the union $t₁ \cup t₂$ is a subset of the union of the pointwise products $s₁ * t₁$ and $s₂ * t₂$. That is, $$ (s₁ \cap s₂) * (t₁ \cup t₂) \subseteq (s₁ * t₁) \cup (s₂ * t₂). $$

Finset.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₂ :=
  image₂_union_inter_subset_union

Subset Property: $(s₁ \cup s₂) * (t₁ \cap t₂) \subseteq s₁ * t₁ \cup s₂ * t₂$

Informal description

For any finite sets $s₁, s₂, t₁, t₂$ of a type $\alpha$ with multiplication, the pointwise product of the union $s₁ \cup s₂$ with the intersection $t₁ \cap t₂$ is a subset of the union of the pointwise products $s₁ * t₁$ and $s₂ * t₂$. In other words: $$ (s₁ \cup s₂) * (t₁ \cap t₂) \subseteq s₁ * t₁ \cup s₂ * t₂ $$

Finset.subset_mul theorem

{s t : Set α} : ↑u ⊆ s * t → ∃ s' t' : Finset α, ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ s' * t'

Full source

/-- If a finset `u` is contained in the product of two sets `s * t`, we can find two finsets `s'`,
`t'` such that `s' ⊆ s`, `t' ⊆ t` and `u ⊆ s' * t'`. -/
@[to_additive
      "If a finset `u` is contained in the sum of two sets `s + t`, we can find two finsets
      `s'`, `t'` such that `s' ⊆ s`, `t' ⊆ t` and `u ⊆ s' + t'`."]
theorem subset_mul {s t : Set α} :
    ↑u ⊆ s * t → ∃ s' t' : Finset α, ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ s' * t' :=
  subset_set_image₂

Finite subset containment in pointwise product of sets

Informal description

Let $u$ be a finite subset of a type $\alpha$ with a multiplication operation, and let $s, t \subseteq \alpha$ be arbitrary subsets. If $u$ is contained in the pointwise product set $s * t = \{x * y \mid x \in s, y \in t\}$, then there exist finite subsets $s' \subseteq s$ and $t' \subseteq t$ such that $u \subseteq s' * t'$.

Finset.image_mul theorem

[DecidableEq β] : (s * t).image (f : α → β) = s.image f * t.image f

Full source

@[to_additive]
theorem image_mul [DecidableEq β] : (s * t).image (f : α → β) = s.image f * t.image f :=
  image_image₂_distrib <| map_mul f

Image of Pointwise Product Equals Pointwise Product of Images

Informal description

Let $\alpha$ and $\beta$ be types with decidable equality on $\beta$, and let $f : \alpha \to \beta$ be a function. For any finite subsets $s, t \subseteq \alpha$, the image of the pointwise product $s * t$ under $f$ equals the pointwise product of the images of $s$ and $t$ under $f$. That is: $$ f(s * t) = f(s) * f(t) $$

Finset.image_op_mul theorem

(s t : Finset α) : (s * t).image op = t.image op * s.image op

Full source

@[to_additive]
lemma image_op_mul (s t : Finset α) : (s * t).image op = t.image op * s.image op :=
  image_image₂_antidistrib op_mul

Image of Pointwise Product under Opposite Map Equals Reversed Product of Images

Informal description

For any finite subsets $s$ and $t$ of a type $\alpha$ with multiplication, the image of their pointwise product $s * t$ under the canonical map $\text{op} : \alpha \to \alpha^\text{op}$ equals the pointwise product of the images of $t$ and $s$ under $\text{op}$ in the multiplicative opposite $\alpha^\text{op}$. That is: $$\text{op}(s * t) = \text{op}(t) * \text{op}(s)$$

Finset.product_mul_product_comm theorem

 [DecidableEq β] (s₁ s₂ : Finset α) (t₁ t₂ : Finset β) : (s₁ ×ˢ t₁) * (s₂ ×ˢ t₂) = (s₁ * s₂) ×ˢ (t₁ * t₂)

Full source

@[to_additive (attr := simp)]
lemma product_mul_product_comm [DecidableEq β] (s₁ s₂ : Finset α) (t₁ t₂ : Finset β) :
    (s₁ ×ˢ t₁) * (s₂ ×ˢ t₂) = (s₁ * s₂) ×ˢ (t₁ * t₂) :=
  mod_cast s₁.toSet.prod_mul_prod_comm s₂ t₁.toSet t₂

Commutativity of Cartesian Product with Pointwise Multiplication for Finite Sets

Informal description

For any finite sets $s_1, s_2$ of type $\alpha$ and $t_1, t_2$ of type $\beta$, the pointwise product of the Cartesian products $s_1 \times t_1$ and $s_2 \times t_2$ is equal to the Cartesian product of the pointwise products $s_1 * s_2$ and $t_1 * t_2$. In symbols: $$(s_1 \times t_1) * (s_2 \times t_2) = (s_1 * s_2) \times (t_1 * t_2)$$

Finset.map_op_mul theorem

(s t : Finset α) : (s * t).map opEquiv.toEmbedding = t.map opEquiv.toEmbedding * s.map opEquiv.toEmbedding

Full source

@[to_additive]
lemma map_op_mul (s t : Finset α) :
    (s * t).map opEquiv.toEmbedding = t.map opEquiv.toEmbedding * s.map opEquiv.toEmbedding := by
  simp [map_eq_image, image_op_mul]

Image of Pointwise Product under Opposite Embedding Equals Reversed Product of Images

Informal description

For any finite subsets $s$ and $t$ of a type $\alpha$ with multiplication, the image of their pointwise product $s * t$ under the canonical embedding $\text{op} : \alpha \hookrightarrow \alpha^\text{op}$ equals the pointwise product of the images of $t$ and $s$ under $\text{op}$ in the multiplicative opposite $\alpha^\text{op}$. That is: $$\text{op}(s * t) = \text{op}(t) * \text{op}(s)$$

Finset.singletonMulHom definition

: α →ₙ* Finset α

Full source

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

Singleton finite set multiplicative homomorphism

Informal description

The function that maps an element $a$ of a multiplicative structure $\alpha$ to the singleton finite set $\{a\}$ is a non-unital multiplicative homomorphism from $\alpha$ to the finite sets of $\alpha$ equipped with pointwise multiplication. This means that for any $a, b \in \alpha$, the image of the product $a * b$ under this function is equal to the pointwise product of the images $\{a\} * \{b\}$.

Finset.coe_singletonMulHom theorem

: (singletonMulHom : α → Finset α) = singleton

Full source

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

Equality of Singleton Multiplicative Homomorphism and Singleton Function

Informal description

The function `singletonMulHom` from a multiplicative structure $\alpha$ to the finite sets of $\alpha$ is equal to the singleton function, which maps each element $a \in \alpha$ to the singleton set $\{a\}$.

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

Informal description

For any element $a$ in a type $\alpha$ with a multiplicative structure, the multiplicative homomorphism `singletonMulHom` maps $a$ to the singleton finite set $\{a\}$.

Finset.imageMulHom definition

[DecidableEq β] : Finset α →ₙ* Finset β

Full source

/-- Lift a `MulHom` to `Finset` via `image`. -/
@[to_additive (attr := simps) "Lift an `AddHom` to `Finset` via `image`"]
def imageMulHom [DecidableEq β] : FinsetFinset α →ₙ* Finset β where
  toFun := Finset.image f
  map_mul' _ _ := image_mul _

Lifting a multiplicative homomorphism to finite sets via pointwise image

Informal description

Given a multiplicative homomorphism $f \colon \alpha \to \beta$ between types with decidable equality on $\beta$, the function `Finset.imageMulHom` lifts $f$ to a non-unital multiplicative homomorphism between the finite sets of $\alpha$ and $\beta$ by applying $f$ pointwise to each element. Specifically, for any finite sets $s, t \subseteq \alpha$, we have: $$ \text{imageMulHom}(s * t) = \text{imageMulHom}(s) * \text{imageMulHom}(t) $$ where the multiplication on finite sets is defined pointwise.

Finset.sup_mul_le theorem

 {β} [SemilatticeSup β] [OrderBot β] {s t : Finset α} {f : α → β} {a : β} :
  sup (s * t) f ≤ a ↔ ∀ x ∈ s, ∀ y ∈ t, f (x * y) ≤ a

Full source

@[to_additive (attr := simp (default + 1))]
lemma sup_mul_le {β} [SemilatticeSup β] [OrderBot β] {s t : Finset α} {f : α → β} {a : β} :
    supsup (s * t) f ≤ a ↔ ∀ x ∈ s, ∀ y ∈ t, f (x * y) ≤ a :=
  sup_image₂_le

Supremum Bound for Pointwise Product: $\sup_{z \in s \cdot t} f(z) \leq a \leftrightarrow \forall x \in s, \forall y \in t, f(x \cdot y) \leq a$

Informal description

Let $\alpha$ and $\beta$ be types, where $\beta$ is a join-semilattice with a least element $\bot$. For any finite sets $s, t \subseteq \alpha$, any function $f : \alpha \to \beta$, and any element $a \in \beta$, the supremum of $f$ over the pointwise product set $s \cdot t$ is less than or equal to $a$ if and only if for all $x \in s$ and $y \in t$, $f(x \cdot y) \leq a$.

Finset.sup_mul_left theorem

 {β} [SemilatticeSup β] [OrderBot β] (s t : Finset α) (f : α → β) : sup (s * t) f = sup s fun x ↦ sup t (f <| x * ·)

Full source

@[to_additive]
lemma sup_mul_left {β} [SemilatticeSup β] [OrderBot β] (s t : Finset α) (f : α → β) :
    sup (s * t) f = sup s fun x ↦ sup t (f <| x * ·) :=
  sup_image₂_left ..

Supremum over Product Set Equals Iterated Supremum (Left Version)

Informal description

Let $\alpha$ and $\beta$ be types, where $\beta$ is equipped with a join-semilattice structure and a bottom element $\bot$. For any finite sets $s, t \subseteq \alpha$ and any function $f : \alpha \to \beta$, the supremum of $f$ over the pointwise product set $s \cdot t$ equals the supremum over $s$ of the functions that take each $x \in s$ to the supremum over $t$ of $f(x \cdot y)$. In other words, \[ \sup_{z \in s \cdot t} f(z) = \sup_{x \in s} \left( \sup_{y \in t} f(x \cdot y) \right). \]

Finset.sup_mul_right theorem

 {β} [SemilatticeSup β] [OrderBot β] (s t : Finset α) (f : α → β) : sup (s * t) f = sup t fun y ↦ sup s (f <| · * y)

Full source

@[to_additive]
lemma sup_mul_right {β} [SemilatticeSup β] [OrderBot β] (s t : Finset α) (f : α → β) :
    sup (s * t) f = sup t fun y ↦ sup s (f <| · * y) :=
  sup_image₂_right ..

Supremum over Product Set Equals Iterated Supremum (Right Version)

Informal description

Let $\alpha$ and $\beta$ be types, where $\beta$ is a join-semilattice with a bottom element $\bot$. For any finite sets $s, t \subseteq \alpha$ and any function $f : \alpha \to \beta$, the supremum of $f$ over the pointwise product set $s \cdot t$ equals the supremum over $t$ of the functions that take each $y \in t$ to the supremum over $s$ of $f(x \cdot y)$. In other words, \[ \sup_{z \in s \cdot t} f(z) = \sup_{y \in t} \left( \sup_{x \in s} f(x \cdot y) \right). \]

Finset.le_inf_mul theorem

 {β} [SemilatticeInf β] [OrderTop β] {s t : Finset α} {f : α → β} {a : β} :
  a ≤ inf (s * t) f ↔ ∀ x ∈ s, ∀ y ∈ t, a ≤ f (x * y)

Full source

@[to_additive (attr := simp (default + 1))]
lemma le_inf_mul {β} [SemilatticeInf β] [OrderTop β] {s t : Finset α} {f : α → β} {a : β} :
    a ≤ inf (s * t) f ↔ ∀ x ∈ s, ∀ y ∈ t, a ≤ f (x * y) :=
  le_inf_image₂

Infimum Bound for Pointwise Product Set: $a \leq \inf_{s \cdot t} f \leftrightarrow \forall x \in s, \forall y \in t, a \leq f(x \cdot y)$

Informal description

Let $\alpha$ be a type with a multiplication operation, and let $\beta$ be a meet-semilattice with a top element $\top$. For any finite sets $s, t \subseteq \alpha$, any function $f \colon \alpha \to \beta$, and any element $a \in \beta$, we have \[ a \leq \inf_{z \in s \cdot t} f(z) \quad \text{if and only if} \quad \forall x \in s, \forall y \in t, a \leq f(x \cdot y). \]

Finset.inf_mul_left theorem

 {β} [SemilatticeInf β] [OrderTop β] (s t : Finset α) (f : α → β) : inf (s * t) f = inf s fun x ↦ inf t (f <| x * ·)

Full source

@[to_additive]
lemma inf_mul_left {β} [SemilatticeInf β] [OrderTop β] (s t : Finset α) (f : α → β) :
    inf (s * t) f = inf s fun x ↦ inf t (f <| x * ·) :=
  inf_image₂_left ..

Infimum over Product Set Equals Iterated Infimum (Left Version)

Informal description

Let $\alpha$ be a type with a multiplication operation, and let $\beta$ be a meet-semilattice with a top element $\top$. For any finite sets $s, t \subseteq \alpha$ and any function $f \colon \alpha \to \beta$, the infimum of $f$ over the pointwise product set $s \cdot t = \{x \cdot y \mid x \in s, y \in t\}$ is equal to the infimum over $s$ of the functions that take each $x \in s$ to the infimum over $t$ of $f(x \cdot y)$. In other words, \[ \inf_{z \in s \cdot t} f(z) = \inf_{x \in s} \left( \inf_{y \in t} f(x \cdot y) \right). \]

Finset.inf_mul_right theorem

 {β} [SemilatticeInf β] [OrderTop β] (s t : Finset α) (f : α → β) : inf (s * t) f = inf t fun y ↦ inf s (f <| · * y)

Full source

@[to_additive]
lemma inf_mul_right {β} [SemilatticeInf β] [OrderTop β] (s t : Finset α) (f : α → β) :
    inf (s * t) f = inf t fun y ↦ inf s (f <| · * y) :=
  inf_image₂_right ..

Infimum over Product Set Equals Iterated Infimum (Right Version)

Informal description

Let $\alpha$ be a type with a multiplication operation, and let $\beta$ be a meet-semilattice with a top element $\top$. For any finite sets $s, t \subseteq \alpha$ and any function $f \colon \alpha \to \beta$, the infimum of $f$ over the pointwise product set $s \cdot t = \{x \cdot y \mid x \in s, y \in t\}$ is equal to the infimum over $t$ of the functions that take each $y \in t$ to the infimum over $s$ of $f(x \cdot y)$. In other words, \[ \inf_{z \in s \cdot t} f(z) = \inf_{y \in t} \left( \inf_{x \in s} f(x \cdot y) \right). \]

Finset.div definition

: Div (Finset α)

Full source

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

Pointwise division of finite sets

Informal description

The pointwise division operation on finite sets $ s $ and $ t $ of type $ \alpha $ (where $ \alpha $ has a division operation) is defined as the finite set consisting of all elements $ x / y $ where $ x \in s $ and $ y \in t $. This operation is implemented using the binary image function applied to the division operation.

Finset.div_def theorem

: s / t = (s ×ˢ t).image fun p : α × α => p.1 / p.2

Full source

@[to_additive]
theorem div_def : s / t = (s ×ˢ t).image fun p : α × α => p.1 / p.2 :=
  rfl

Definition of Pointwise Division for Finite Sets via Cartesian Product and Image

Informal description

For any two finite sets $s$ and $t$ of elements in a type $\alpha$ equipped with a division operation, the pointwise division $s / t$ is equal to the image of the function $(x, y) \mapsto x / y$ applied to the Cartesian product $s \times t$.

Finset.image_div_product theorem

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

Full source

@[to_additive]
theorem image_div_product : ((s ×ˢ t).image fun x : α × α => x.fst / x.snd) = s / t :=
  rfl

Image of Cartesian Product under Division Equals Pointwise Division of Finite Sets

Informal description

For finite sets $s$ and $t$ of a type $\alpha$ equipped 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 $s / t$.

Finset.mem_div theorem

: a ∈ s / t ↔ ∃ b ∈ s, ∃ c ∈ t, b / c = a

Full source

@[to_additive]
theorem mem_div : a ∈ s / ta ∈ s / t ↔ ∃ b ∈ s, ∃ c ∈ t, b / c = a :=
  mem_image₂

Membership Criterion for Pointwise Division of Finite Sets

Informal description

An element $a$ belongs to the pointwise division $s / t$ of two finite sets $s$ and $t$ if and only if there exist elements $b \in s$ and $c \in t$ such that $b / c = a$.

Finset.coe_div theorem

(s t : Finset α) : (↑(s / t) : Set α) = ↑s / ↑t

Full source

@[to_additive (attr := simp, norm_cast)]
theorem coe_div (s t : Finset α) : (↑(s / t) : Set α) = ↑s / ↑t :=
  coe_image₂ _ _ _

Equality of Pointwise Division of Finite Sets and Their Underlying Sets

Informal description

For any two finite sets $s$ and $t$ of a type $\alpha$ equipped with a division operation, the underlying set of the pointwise division $s / t$ is equal to the pointwise division of the underlying sets of $s$ and $t$. That is, $\overline{s / t} = \overline{s} / \overline{t}$, where $\overline{\cdot}$ denotes the conversion from a finite set to a set.

Finset.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_image₂_of_mem

Closure of Pointwise Division under Membership

Informal description

For any elements $a \in s$ and $b \in t$ in finite sets $s$ and $t$ respectively, the element $a / b$ belongs to the pointwise division $s / t$.

Finset.div_card_le theorem

: #(s / t) ≤ #s * #t

Full source

@[to_additive]
theorem div_card_le : #(s / t) ≤ #s * #t :=
  card_image₂_le _ _ _

Cardinality Bound for Pointwise Division of Finite Sets: $|s / t| \leq |s| \cdot |t|$

Informal description

For any two finite sets $s$ and $t$ of a type $\alpha$ equipped with a division operation, the cardinality of their pointwise division set $s / t$ is bounded by the product of their cardinalities, i.e., \[ |s / t| \leq |s| \cdot |t|. \]

Finset.empty_div theorem

(s : Finset α) : ∅ / s = ∅

Full source

@[to_additive (attr := simp)]
theorem empty_div (s : Finset α) : ∅ / s = ∅ :=
  image₂_empty_left

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

Informal description

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

Finset.div_empty theorem

(s : Finset α) : s / ∅ = ∅

Full source

@[to_additive (attr := simp)]
theorem div_empty (s : Finset α) : s / ∅ = ∅ :=
  image₂_empty_right

Pointwise Division by Empty Set Yields Empty Set

Informal description

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

Finset.div_eq_empty theorem

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

Full source

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

Empty Pointwise Division Criterion for Finite Sets

Informal description

For any two finite sets $s$ and $t$ of a type $\alpha$ equipped with a division operation, the pointwise division set $s / 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 $$

Finset.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 :=
  image₂_nonempty_iff

Nonemptiness Criterion for Pointwise Division of Finite Sets

Informal description

For any two finite sets $s$ and $t$ of a type $\alpha$ equipped with a division operation, the pointwise division set $s / t$ is nonempty if and only if both $s$ and $t$ are nonempty. That is: $$ s / t \neq \emptyset \leftrightarrow s \neq \emptyset \land t \neq \emptyset $$

Finset.Nonempty.div theorem

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

Full source

@[to_additive (attr := aesop safe apply (rule_sets := [finsetNonempty]))]
theorem Nonempty.div : s.Nonempty → t.Nonempty → (s / t).Nonempty :=
  Nonempty.image₂

Nonemptiness of Pointwise Division for Nonempty Finite Sets

Informal description

For any two finite sets $s$ and $t$ of a type $\alpha$ equipped with a division operation, if both $s$ and $t$ are nonempty, then their pointwise division set $s / t$ is also nonempty.

Finset.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_image₂_left

Nonemptiness of Left Set in Nonempty Pointwise Division of Finite Sets

Informal description

For any two finite sets $s$ and $t$ of a type $\alpha$ equipped with a division operation, if the pointwise division set $s / t$ is nonempty, then $s$ is nonempty. That is: $$ s / t \neq \emptyset \implies s \neq \emptyset $$

Finset.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_image₂_right

Nonempty Right Set in Pointwise Division of Finite Sets

Informal description

For any finite sets $s$ and $t$ of elements of a type $\alpha$ with a division operation, if the pointwise division set $s / t$ is nonempty, then the set $t$ is nonempty.

Finset.div_singleton theorem

(a : α) : s / { a } = s.image (· / a)

Full source

@[to_additive (attr := simp)]
theorem div_singleton (a : α) : s / {a} = s.image (· / a) :=
  image₂_singleton_right

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

Informal description

For any finite set $s$ of elements of type $\alpha$ (where $\alpha$ has a division operation) and any element $a \in \alpha$, the pointwise division of $s$ by the singleton set $\{a\}$ is equal to the image of the function $\lambda x, x / a$ applied to $s$.

Finset.singleton_div theorem

(a : α) : { a } / s = s.image (a / ·)

Full source

@[to_additive (attr := simp)]
theorem singleton_div (a : α) : {a} / s = s.image (a / ·) :=
  image₂_singleton_left

Pointwise Division of Singleton by Finite Set

Informal description

For any element $a$ in a type $\alpha$ with a division operation and any finite subset $s \subseteq \alpha$, the pointwise division of the singleton set $\{a\}$ by $s$ is equal to the image of $s$ under the function $a / \cdot$, i.e., $\{a\} / s = \{a / x \mid x \in s\}$.

Finset.singleton_div_singleton theorem

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

Full source

@[to_additive]
theorem singleton_div_singleton (a b : α) : ({a} : Finset α) / {b} = {a / b} :=
  image₂_singleton

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

Informal description

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

Finset.div_subset_div theorem

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

Full source

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

Monotonicity of Pointwise Division under Subset Inclusion

Informal description

For any finite sets $s_1, s_2, t_1, t_2$ of a type $\alpha$ with a division operation, if $s_1 \subseteq s_2$ and $t_1 \subseteq t_2$, then the pointwise division $s_1 / t_1$ is a subset of $s_2 / t_2$.

Finset.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₂ :=
  image₂_subset_left

Left Monotonicity of Pointwise Division under Right Subset Inclusion

Informal description

For any finite sets $s$, $t_1$, and $t_2$ of a type $\alpha$ with a division operation, if $t_1 \subseteq t_2$, then the pointwise division $s / t_1$ is a subset of $s / t_2$.

Finset.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 :=
  image₂_subset_right

Right Monotonicity of Pointwise Division for Finite Sets

Informal description

For any finite sets $s_1, s_2, t$ of a type $\alpha$ with a division operation, if $s_1 \subseteq s_2$, then the pointwise division $s_1 / t$ is a subset of $s_2 / t$.

Finset.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 :=
  image₂_subset_iff

Subset Criterion for Pointwise Division of Finite Sets: $s / t \subseteq u \leftrightarrow \forall x \in s, \forall y \in t, x / y \in u$

Informal description

For finite sets $s$, $t$, and $u$ of a type $\alpha$ with a division operation, the pointwise division $s / t$ is a subset of $u$ if and only if for every $x \in s$ and $y \in t$, the element $x / y$ belongs to $u$.

Finset.union_div theorem

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

Full source

@[to_additive]
theorem union_div : (s₁ ∪ s₂) / t = s₁ / t ∪ s₂ / t :=
  image₂_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 finite sets $s_1, s_2, t$ of a type $\alpha$ with a division operation, the pointwise division of the union $s_1 \cup s_2$ by $t$ is equal to 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).$$

Finset.div_union theorem

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

Full source

@[to_additive]
theorem div_union : s / (t₁ ∪ t₂) = s / t₁ ∪ s / t₂ :=
  image₂_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 finite sets $s, t_1, t_2$ of a type $\alpha$ with a division operation, the pointwise division of $s$ by the union $t_1 \cup t_2$ is equal to 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. \]

Finset.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) :=
  image₂_inter_subset_left

Subset Property for Pointwise Division of Intersection: $(s_1 \cap s_2) / t \subseteq (s_1 / t) \cap (s_2 / t)$

Informal description

For any finite sets $s_1, s_2, t$ of a type $\alpha$ 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).$$

Finset.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₂) :=
  image₂_inter_subset_right

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

Informal description

For any finite sets $s, t_1, t_2$ of a type $\alpha$ 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. \]

Finset.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₂ :=
  image₂_inter_union_subset_union

Subset Property for Pointwise Division of Intersection by Union in Finite Sets

Informal description

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

Finset.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₂ :=
  image₂_union_inter_subset_union

Subset Property of Pointwise Division over Union and Intersection

Informal description

For any finite sets $s_1, s_2, t_1, t_2$ of a type $\alpha$ 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$. In other words, $$(s_1 \cup s_2) / (t_1 \cap t_2) \subseteq (s_1 / t_1) \cup (s_2 / t_2).$$

Finset.subset_div theorem

{s t : Set α} : ↑u ⊆ s / t → ∃ s' t' : Finset α, ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ s' / t'

Full source

/-- If a finset `u` is contained in the product of two sets `s / t`, we can find two finsets `s'`,
`t'` such that `s' ⊆ s`, `t' ⊆ t` and `u ⊆ s' / t'`. -/
@[to_additive
      "If a finset `u` is contained in the sum of two sets `s - t`, we can find two finsets
      `s'`, `t'` such that `s' ⊆ s`, `t' ⊆ t` and `u ⊆ s' - t'`."]
theorem subset_div {s t : Set α} :
    ↑u ⊆ s / t → ∃ s' t' : Finset α, ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ s' / t' :=
  subset_set_image₂

Finite Subset Containment in Pointwise Division of Sets

Informal description

For any finite set $u$ of a type $\alpha$ with a division operation, if $u$ is contained in the pointwise division $s / t$ of two sets $s, t \subseteq \alpha$, then there exist finite subsets $s' \subseteq s$ and $t' \subseteq t$ such that $u \subseteq s' / t'$.

Finset.sup_div_le theorem

 [SemilatticeSup β] [OrderBot β] {s t : Finset α} {f : α → β} {a : β} :
  sup (s / t) f ≤ a ↔ ∀ x ∈ s, ∀ y ∈ t, f (x / y) ≤ a

Full source

@[to_additive (attr := simp (default + 1))]
lemma sup_div_le [SemilatticeSup β] [OrderBot β] {s t : Finset α} {f : α → β} {a : β} :
    supsup (s / t) f ≤ a ↔ ∀ x ∈ s, ∀ y ∈ t, f (x /  y) ≤ a :=
  sup_image₂_le

Supremum Bound for Pointwise Division of Finite Sets: $\sup_{s/t} f \leq a \leftrightarrow \forall x \in s, \forall y \in t, f(x/y) \leq a$

Informal description

Let $\alpha$ and $\beta$ be types, where $\beta$ is a join-semilattice with a bottom element $\bot$. For any finite sets $s, t \subseteq \alpha$, any function $f : \alpha \to \beta$, and any element $a \in \beta$, the supremum of $f$ over the pointwise division set $s / t = \{x / y \mid x \in s, y \in t\}$ satisfies \[ \sup_{z \in s / t} f(z) \leq a \] if and only if for all $x \in s$ and $y \in t$, we have $f(x / y) \leq a$.

Finset.sup_div_left theorem

 [SemilatticeSup β] [OrderBot β] (s t : Finset α) (f : α → β) : sup (s / t) f = sup s fun x ↦ sup t (f <| x / ·)

Full source

@[to_additive]
lemma sup_div_left [SemilatticeSup β] [OrderBot β] (s t : Finset α) (f : α → β) :
    sup (s / t) f = sup s fun x ↦ sup t (f <| x / ·) :=
  sup_image₂_left ..

Supremum Decomposition for Pointwise Division of Finite Sets (Left Version)

Informal description

Let $\alpha$ and $\beta$ be types, where $\beta$ is a join-semilattice with a bottom element $\bot$. For any finite sets $s, t \subseteq \alpha$ and any function $f : \alpha \to \beta$, the supremum of $f$ over the pointwise division set $s / t = \{x / y \mid x \in s, y \in t\}$ is equal to the supremum over $s$ of the functions that take each $x \in s$ to the supremum over $t$ of $f(x / y)$. In other words, \[ \sup_{z \in s / t} f(z) = \sup_{x \in s} \left( \sup_{y \in t} f(x / y) \right). \]

Finset.sup_div_right theorem

 [SemilatticeSup β] [OrderBot β] (s t : Finset α) (f : α → β) : sup (s / t) f = sup t fun y ↦ sup s (f <| · / y)

Full source

@[to_additive]
lemma sup_div_right [SemilatticeSup β] [OrderBot β] (s t : Finset α) (f : α → β) :
    sup (s / t) f = sup t fun y ↦ sup s (f <| · / y) :=
  sup_image₂_right ..

Supremum Decomposition for Pointwise Division of Finite Sets (Right Version)

Informal description

Let $\alpha$ and $\beta$ be types, where $\beta$ is a join-semilattice with a bottom element $\bot$. For any finite sets $s, t \subseteq \alpha$ and any function $f : \alpha \to \beta$, the supremum of $f$ over the pointwise division set $s / t = \{x / y \mid x \in s, y \in t\}$ is equal to the supremum over $t$ of the functions that take each $y \in t$ to the supremum over $s$ of $f(x / y)$. In other words, \[ \sup_{z \in s / t} f(z) = \sup_{y \in t} \left( \sup_{x \in s} f(x / y) \right). \]

Finset.le_inf_div theorem

 [SemilatticeInf β] [OrderTop β] {s t : Finset α} {f : α → β} {a : β} :
  a ≤ inf (s / t) f ↔ ∀ x ∈ s, ∀ y ∈ t, a ≤ f (x / y)

Full source

@[to_additive (attr := simp (default + 1))]
lemma le_inf_div [SemilatticeInf β] [OrderTop β] {s t : Finset α} {f : α → β} {a : β} :
    a ≤ inf (s / t) f ↔ ∀ x ∈ s, ∀ y ∈ t, a ≤ f (x / y) :=
  le_inf_image₂

Infimum Bound for Pointwise Division of Finite Sets: $a \leq \inf_{s/t} f \leftrightarrow \forall x \in s, \forall y \in t, a \leq f(x/y)$

Informal description

Let $\alpha$ and $\beta$ be types, where $\beta$ is a meet-semilattice with a top element $\top$. For any finite sets $s, t \subseteq \alpha$, any function $f \colon \alpha \to \beta$, and any element $a \in \beta$, we have \[ a \leq \inf_{z \in s / t} f(z) \quad \text{if and only if} \quad \forall x \in s, \forall y \in t, \ a \leq f(x / y), \] where $s / t = \{x / y \mid x \in s, y \in t\}$ denotes the pointwise division of $s$ and $t$.

Finset.inf_div_left theorem

 [SemilatticeInf β] [OrderTop β] (s t : Finset α) (f : α → β) : inf (s / t) f = inf s fun x ↦ inf t (f <| x / ·)

Full source

@[to_additive]
lemma inf_div_left [SemilatticeInf β] [OrderTop β] (s t : Finset α) (f : α → β) :
    inf (s / t) f = inf s fun x ↦ inf t (f <| x / ·) :=
  inf_image₂_left ..

Infimum Decomposition for Pointwise Division of Finite Sets (Left Version)

Informal description

Let $\alpha$ and $\beta$ be types, where $\beta$ is a meet-semilattice with a top element $\top$. For any finite sets $s, t \subseteq \alpha$ and any function $f : \alpha \to \beta$, the infimum of $f$ over the pointwise division set $s / t = \{x / y \mid x \in s, y \in t\}$ is equal to the infimum over $s$ of the functions that take each $x \in s$ to the infimum over $t$ of $f(x / y)$. In other words, \[ \inf_{z \in s / t} f(z) = \inf_{x \in s} \left( \inf_{y \in t} f(x / y) \right). \]

Finset.inf_div_right theorem

 [SemilatticeInf β] [OrderTop β] (s t : Finset α) (f : α → β) : inf (s / t) f = inf t fun y ↦ inf s (f <| · / y)

Full source

@[to_additive]
lemma inf_div_right [SemilatticeInf β] [OrderTop β] (s t : Finset α) (f : α → β) :
    inf (s / t) f = inf t fun y ↦ inf s (f <| · / y) :=
  inf_image₂_right ..

Infimum Decomposition for Pointwise Division of Finite Sets (Right Version)

Informal description

Let $\alpha$ and $\beta$ be types, where $\beta$ is a meet-semilattice with a top element $\top$. For any finite sets $s, t \subseteq \alpha$ and any function $f : \alpha \to \beta$, the infimum of $f$ over the pointwise division set $s / t = \{x / y \mid x \in s, y \in t\}$ is equal to the infimum over $t$ of the functions that take each $y \in t$ to the infimum over $s$ of $f(x / y)$. In other words, \[ \inf_{z \in s / t} f(z) = \inf_{y \in t} \left( \inf_{x \in s} f(x / y) \right). \]

Finset.nsmul definition

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

Full source

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

Repeated pointwise addition of a finite set

Informal description

The definition `Finset.nsmul` provides a scalar multiplication operation for finite sets, where for a natural number `n` and a finite set `s` of elements in a type `α` with zero and addition, `n • s` is defined as the repeated pointwise addition of `s` with itself `n` times. This operation is implemented using the function `nsmulRec`, which recursively computes the sum `s + s + ... + s` with `n` terms.

Finset.npow definition

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

Full source

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

Repeated pointwise multiplication of a finite set

Informal description

The power operation on finite sets, where for a finite set $ s $ of type $ \alpha $ and a natural number $ n $, the power $ s^n $ is defined as the repeated pointwise multiplication of $ s $ with itself $ n $ times. Specifically: - For $ n = 0 $, it returns the singleton set containing the multiplicative identity $ \{1\} $. - For $ n + 1 $, it recursively computes the pointwise product $ s^n * s $. Note that this operation differs from the pointwise scaling operation, which would instead scale each element of $ s $ by $ n $. For example, $ 2 \cdot \{1, 2\} $ under pointwise scaling is $ \{2, 4\} $, whereas under repeated pointwise multiplication it is $ \{2, 3, 4\} $.

Finset.zsmul definition

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

Full source

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

Integer scalar multiplication of a finite set

Informal description

The function defines the scalar multiplication of an integer `n` with a finite set `s` in a type `α` equipped with zero, addition, and negation. For each element `x ∈ s`, the result is the finite set consisting of all `n • x` (scalar multiplication of `n` with `x`), where the operation `•` is defined via repeated addition/subtraction based on the sign of `n`.

Finset.zpow definition

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

Full source

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

Integer power operation on finite sets

Informal description

The integer power operation on finite sets, where for a finite set $s$ of elements from a type $\alpha$ with multiplicative identity, multiplication, and inversion, and an integer $n$, the power $s^n$ is defined as the finite set consisting of all elements $x^n$ with $x \in s$. This operation is defined recursively using the `zpowRec` function, which extends the natural number power operation `npowRec` to integers.

Finset.semigroup definition

[Semigroup α] : Semigroup (Finset α)

Full source

/-- `Finset α` is a `Semigroup` under pointwise operations if `α` is. -/
@[to_additive "`Finset α` is an `AddSemigroup` under pointwise operations if `α` is. "]
protected def semigroup [Semigroup α] : Semigroup (Finset α) :=
  coe_injective.semigroup _ coe_mul

Semigroup structure on finite sets under pointwise multiplication

Informal description

For a semigroup $\alpha$, the type of finite subsets of $\alpha$ forms a semigroup under pointwise multiplication, where the product of two finite sets $s$ and $t$ is the finite set $\{x * y \mid x \in s, y \in t\}$.

Finset.commSemigroup definition

: CommSemigroup (Finset α)

Full source

/-- `Finset α` is a `CommSemigroup` under pointwise operations if `α` is. -/
@[to_additive "`Finset α` is an `AddCommSemigroup` under pointwise operations if `α` is. "]
protected def commSemigroup : CommSemigroup (Finset α) :=
  coe_injective.commSemigroup _ coe_mul

Finite sets as a commutative semigroup under pointwise multiplication

Informal description

The type of finite subsets of a type $\alpha$ forms a commutative semigroup under pointwise multiplication when $\alpha$ is a commutative semigroup. Specifically, for finite sets $s$ and $t$ of $\alpha$, the product $s * t$ is defined as the finite set consisting of all elements $x * y$ with $x \in s$ and $y \in t$.

Finset.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 :=
  image₂_inter_union_subset mul_comm

Subset property for pointwise product of intersection and union in finite sets

Informal description

For any finite 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) * (s \cup t) \subseteq s * t. \]

Finset.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 :=
  image₂_union_inter_subset mul_comm

Subset property: $(s \cup t) * (s \cap t) \subseteq s * t$ in commutative semigroups

Informal description

For any finite 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) * (s \cap t) \subseteq s * t.$$

Finset.mulOneClass definition

: MulOneClass (Finset α)

Full source

/-- `Finset α` is a `MulOneClass` under pointwise operations if `α` is. -/
@[to_additive "`Finset α` is an `AddZeroClass` under pointwise operations if `α` is."]
protected def mulOneClass : MulOneClass (Finset α) :=
  coe_injective.mulOneClass _ (coe_singleton 1) coe_mul

Pointwise multiplicative structure with identity on finite sets

Informal description

The structure `Finset α` forms a `MulOneClass` under pointwise operations when `α` is a `MulOneClass`. Specifically, the multiplicative identity is the singleton set `{1}`, and multiplication is defined pointwise as `s * t = {x * y | x ∈ s, y ∈ t}` for any finite sets `s, t ⊆ α`.

Finset.subset_mul_left theorem

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

Full source

@[to_additive]
theorem subset_mul_left (s : Finset α) {t : Finset α} (ht : (1 : α) ∈ t) : s ⊆ s * t := fun a ha =>
  mem_mul.2 ⟨a, ha, 1, ht, mul_one _⟩

Left Subset Property of Pointwise Multiplication with Identity

Informal description

For any finite set $s$ of elements in a multiplicative monoid $\alpha$, and any finite set $t$ containing the multiplicative identity $1$, the set $s$ is a subset of the pointwise product $s * t$.

Finset.subset_mul_right theorem

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

Full source

@[to_additive]
theorem subset_mul_right {s : Finset α} (t : Finset α) (hs : (1 : α) ∈ s) : t ⊆ s * t := fun a ha =>
  mem_mul.2 ⟨1, hs, a, ha, one_mul _⟩

Right Multiplication by Identity-Containing Set Preserves Inclusion

Informal description

For any finite set $t$ of elements in a multiplicative monoid $\alpha$, and any finite set $s \subseteq \alpha$ containing the multiplicative identity $1$, the set $t$ is a subset of the pointwise product $s * t$.

Finset.singletonMonoidHom definition

: α →* Finset α

Full source

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

Singleton monoid homomorphism for finite sets

Informal description

The function that maps an element $ a $ of a monoid $ \alpha $ to the singleton finite set $ \{a\} $ is a monoid homomorphism from $ \alpha $ to the finite sets of $ \alpha $ equipped with pointwise multiplication. This means it preserves both the multiplicative identity ($ \{1\} $) and the multiplication operation ($ \{a * b\} = \{a\} * \{b\} $ for all $ a, b \in \alpha $).

Finset.coe_singletonMonoidHom theorem

: (singletonMonoidHom : α → Finset α) = singleton

Full source

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

Singleton Monoid Homomorphism Equals Singleton Function

Informal description

The monoid homomorphism that maps an element $a$ of a monoid $\alpha$ to the singleton finite set $\{a\}$ is equal to the singleton function $\alpha \to \text{Finset }\alpha$.

Finset.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 `singletonMonoidHom` maps $a$ to the singleton finite set $\{a\}$.

Finset.coeMonoidHom definition

: Finset α →* Set α

Full source

/-- The coercion from `Finset` to `Set` as a `MonoidHom`. -/
@[to_additive "The coercion from `Finset` to `set` as an `AddMonoidHom`."]
noncomputable def coeMonoidHom : FinsetFinset α →* Set α where
  toFun := (↑)
  map_one' := coe_one
  map_mul' := coe_mul

Finite set to set monoid homomorphism

Informal description

The function `Finset.coeMonoidHom` is a monoid homomorphism that converts a finite set `s` of type `α` to the corresponding set `{a | a ∈ s}`. It preserves the multiplicative identity and multiplication, meaning: 1. The image of the singleton `{1}` under this homomorphism is the set `{1}`. 2. For any two finite sets `s` and `t`, the image of their pointwise product `s * t` is the set `{x * y | x ∈ s, y ∈ t}`.

Finset.coe_coeMonoidHom theorem

: (coeMonoidHom : Finset α → Set α) = (↑)

Full source

@[to_additive (attr := simp)]
theorem coe_coeMonoidHom : (coeMonoidHom : Finset α → Set α) = (↑) :=
  rfl

Equality of Finite Set to Set Monoid Homomorphism and Coercion Function

Informal description

The monoid homomorphism `coeMonoidHom` from finite sets to sets, which maps a finite set `s` to the corresponding set `{a | a ∈ s}`, is equal to the coercion function `(↑)` that converts a finite set to a set.

Finset.coeMonoidHom_apply theorem

(s : Finset α) : coeMonoidHom s = s

Full source

@[to_additive (attr := simp)]
theorem coeMonoidHom_apply (s : Finset α) : coeMonoidHom s = s :=
  rfl

Monoid Homomorphism Application to Finite Set

Informal description

For any finite set $s$ of type $\alpha$, the monoid homomorphism `coeMonoidHom` maps $s$ to the corresponding set $\{a \mid a \in s\}$.

Finset.imageMonoidHom definition

[MulOneClass β] [FunLike F α β] [MonoidHomClass F α β] (f : F) : Finset α →* Finset β

Full source

/-- Lift a `MonoidHom` to `Finset` via `image`. -/
@[to_additive (attr := simps) "Lift an `add_monoid_hom` to `Finset` via `image`"]
def imageMonoidHom [MulOneClass β] [FunLike F α β] [MonoidHomClass F α β] (f : F) :
    FinsetFinset α →* Finset β :=
  { imageMulHom f, imageOneHom f with }

Lifting a monoid homomorphism to finite sets via pointwise image

Informal description

Given a monoid homomorphism $ f \colon \alpha \to \beta $ between types with multiplicative structures, the function `Finset.imageMonoidHom` lifts $ f $ to a monoid homomorphism between the finite sets of $ \alpha $ and $ \beta $ by applying $ f $ pointwise to each element. Specifically, for any finite sets $ s, t \subseteq \alpha $, we have: \[ \text{imageMonoidHom}(f)(s * t) = \text{imageMonoidHom}(f)(s) * \text{imageMonoidHom}(f)(t) \] and \[ \text{imageMonoidHom}(f)(\{1\}) = \{1\}, \] where the multiplication and identity on finite sets are defined pointwise.

Finset.coe_pow theorem

(s : Finset α) (n : ℕ) : ↑(s ^ n) = (s : Set α) ^ n

Full source

@[to_additive (attr := simp, norm_cast)]
theorem coe_pow (s : Finset α) (n : ℕ) : ↑(s ^ n) = (s : Set α) ^ n := by
  change ↑(npowRec n s) = (s : Set α) ^ n
  induction' n with n ih
  · rw [npowRec, pow_zero, coe_one]
  · rw [npowRec, pow_succ, coe_mul, ih]

Equality of Pointwise Powers: $\overline{s^n} = \overline{s}^n$

Informal description

For any finite set $s$ of a type $\alpha$ equipped with multiplication and any natural number $n$, the underlying set of the $n$-th power of $s$ (defined by repeated pointwise multiplication) is equal to the $n$-th power of the underlying set of $s$. That is, $\overline{s^n} = \overline{s}^n$, where $\overline{\cdot}$ denotes the underlying set of a finite set.

Finset.monoid definition

: Monoid (Finset α)

Full source

/-- `Finset α` is a `Monoid` under pointwise operations if `α` is. -/
@[to_additive "`Finset α` is an `AddMonoid` under pointwise operations if `α` is. "]
protected def monoid : Monoid (Finset α) :=
  coe_injective.monoid _ coe_one coe_mul coe_pow

Monoid structure on finite sets under pointwise operations

Informal description

The type `Finset α` of finite subsets of a type `α` forms a monoid under pointwise operations when `α` is a monoid. Specifically: - The multiplication of two finite sets `s` and `t` is the finite set consisting of all products `x * y` where `x ∈ s` and `y ∈ t`. - The multiplicative identity is the singleton set `{1}`, where `1` is the identity element of `α`. - The power operation `s^n` is defined as the repeated pointwise multiplication of `s` with itself `n` times.

Finset.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 Finite Set Powers: $1 \in s \implies (m \leq n \Rightarrow s^m \subseteq s^n)$

Informal description

For any finite set $s$ of elements in 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$.

Finset.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 := subset_of_le (pow_left_mono n hst)

Monotonicity of Finite Set Powers under Subset Relation: $s \subseteq t \implies s^n \subseteq t^n$

Informal description

For any finite sets $s$ and $t$ of elements in a monoid $\alpha$, if $s \subseteq t$, then for any natural number $n$, the $n$-th power of $s$ under pointwise multiplication is a subset of the $n$-th power of $t$, i.e., $s^n \subseteq t^n$.

Finset.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 :=
  Finset.pow_right_monotone hs hmn

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

Informal description

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

Finset.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 Finite Set Powers: $s \subseteq t \land 1 \in t \implies s^m \subseteq t^n$ for $m \leq n$

Informal description

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

Finset.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 Finite Set in Its Power: $1 \in s \implies s \subseteq s^n$ for $n \neq 0$

Informal description

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

Finset.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 := subset_of_le (pow_le_pow_mul_of_sq_le_mul hst hn)

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

Informal description

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

Finset.empty_pow theorem

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

Full source

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

Empty Finset Power Law: $\emptyset^n = \emptyset$ for $n \neq 0$

Informal description

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

Finset.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 Finite Sets Remain Nonempty Under Powers

Informal description

For any nonempty finite set $s$ in a monoid $\alpha$ and any natural number $n$, the $n$-th power of $s$ under pointwise multiplication is nonempty.

Finset.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)
    -- TODO: The `nonempty_iff_ne_empty` would be unnecessary if `push_neg` knew how to simplify
    -- `s ≠ ∅` to `s.Nonempty` when `s : Finset α`.
    -- See https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/push_neg.20extensibility
    · exact nonempty_iff_ne_empty.1 (nonempty_iff_ne_empty.2 hs).pow
    · rw [← nonempty_iff_ne_empty]
      simp
  · rintro ⟨rfl, hn⟩
    exact empty_pow hn

Empty Power Condition for Finite Sets: $s^n = \emptyset \iff s = \emptyset \land n \neq 0$

Informal description

For any finite set $s$ of a type $\alpha$ with a monoid structure and any natural number $n$, the $n$-th power of $s$ under pointwise multiplication is empty if and only if $s$ is empty and $n$ is nonzero.

Finset.singleton_pow theorem

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

Full source

@[to_additive (attr := simp) nsmul_singleton]
lemma singleton_pow (a : α) : ∀ n, ({a} : Finset α) ^ 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 type $\alpha$ with a monoid structure 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\}$, where $a^n$ denotes the $n$-th power of $a$ in the monoid $\alpha$.

Finset.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 Finite Set Power: $a \in s \implies a^n \in s^n$

Informal description

For any element $a$ in a finite set $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$.

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

Multiplicative Identity in Finite Set Powers: $1 \in s \implies 1 \in s^n$

Informal description

For any finite set $s$ of elements in a monoid $\alpha$ such that the multiplicative identity $1$ is in $s$, and for any natural number $n$, the multiplicative identity $1$ is in the $n$-th power of $s$ under pointwise multiplication, i.e., $1 \in s^n$.

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

Intersection of Finite Set Powers: $(s \cap t)^n \subseteq s^n \cap t^n$

Informal description

For any finite sets $s$ and $t$ of elements in a monoid $\alpha$ and any natural number $n$, the $n$-th power of the intersection $s \cap t$ under pointwise multiplication is a subset of the intersection of the $n$-th powers of $s$ and $t$, i.e., $(s \cap t)^n \subseteq s^n \cap t^n$.

Finset.coe_list_prod theorem

(s : List (Finset α)) : (↑s.prod : Set α) = (s.map (↑)).prod

Full source

@[to_additive (attr := simp, norm_cast)]
theorem coe_list_prod (s : List (Finset α)) : (↑s.prod : Set α) = (s.map (↑)).prod :=
  map_list_prod (coeMonoidHom : FinsetFinset α →* Set α) _

Equality of Set Product and Product of Sets for Finite Sets

Informal description

For any list $s$ of finite subsets of a type $\alpha$, the underlying set of the product of the list (under pointwise multiplication) is equal to the product of the list obtained by mapping each finite set in $s$ to its underlying set. That is, \[ \left( \prod_{t \in s} t \right) = \prod_{t \in s} \{x \mid x \in t\}, \] where the product on the left is the pointwise product of finite sets and the product on the right is the pointwise product of sets.

Finset.mem_prod_list_ofFn theorem

 {a : α} {s : Fin n → Finset α} :
  a ∈ (List.ofFn s).prod ↔ ∃ f : ∀ i : Fin n, s i, (List.ofFn fun i => (f i : α)).prod = a

Full source

@[to_additive]
theorem mem_prod_list_ofFn {a : α} {s : Fin n → Finset α} :
    a ∈ (List.ofFn s).proda ∈ (List.ofFn s).prod ↔ ∃ f : ∀ i : Fin n, s i, (List.ofFn fun i => (f i : α)).prod = a := by
  rw [← mem_coe, coe_list_prod, List.map_ofFn, Set.mem_prod_list_ofFn]
  rfl

Characterization of Elements in Product of Finite Sets via List Construction

Informal description

For any element $a$ of type $\alpha$ and any finite family of finite sets $s_i$ indexed by $\mathrm{Fin}\,n$, the element $a$ belongs to the product of the list of finite sets $\prod_{i=0}^{n-1} s_i$ if and only if there exists a function $f \colon \mathrm{Fin}\,n \to \alpha$ such that $f(i) \in s_i$ for each $i$ and the product of the list $(f(0), \dots, f(n-1))$ equals $a$. That is, \[ a \in \prod_{i=0}^{n-1} s_i \iff \exists f \colon \mathrm{Fin}\,n \to \alpha, \ (\forall i, f(i) \in s_i) \land \prod_{i=0}^{n-1} f(i) = a. \]

Finset.mem_pow theorem

{a : α} {n : ℕ} : a ∈ s ^ n ↔ ∃ f : Fin n → s, (List.ofFn fun i => ↑(f i)).prod = a

Full source

@[to_additive]
theorem mem_pow {a : α} {n : ℕ} :
    a ∈ s ^ na ∈ s ^ n ↔ ∃ f : Fin n → s, (List.ofFn fun i => ↑(f i)).prod = a := by
  simp [← mem_coe, coe_pow, Set.mem_pow]

Characterization of Elements in Finite Set Powers: $a \in s^n \iff \exists f \colon \mathrm{Fin}\,n \to s,\ \prod f = a$

Informal description

For any element $a$ of type $\alpha$ and natural number $n$, the element $a$ belongs to the $n$-th power of the finite set $s$ (under repeated pointwise multiplication) if and only if there exists a function $f \colon \mathrm{Fin}\,n \to s$ such that the product of the list formed by applying $f$ to each index equals $a$. That is, \[ a \in s^n \iff \exists f \colon \mathrm{Fin}\,n \to s,\ \prod_{i=0}^{n-1} f(i) = a. \]

Finset.card_pow_le theorem

: ∀ {n}, #(s ^ n) ≤ #s ^ n

Full source

@[to_additive]
lemma card_pow_le : ∀ {n}, #(s ^ n) ≤ #s ^ n
  | 0 => by simp
  | n + 1 => by rw [pow_succ, pow_succ]; refine card_mul_le.trans (by gcongr; exact card_pow_le)

Cardinality Bound for Powers of Finite Sets: $|s^n| \leq |s|^n$

Informal description

For any finite set $s$ and natural number $n$, the cardinality of the $n$-th power of $s$ under pointwise multiplication is bounded by the $n$-th power of the cardinality of $s$, i.e., \[ |s^n| \leq |s|^n. \]

Finset.mul_univ_of_one_mem theorem

[Fintype α] (hs : (1 : α) ∈ s) : s * univ = univ

Full source

@[to_additive]
theorem mul_univ_of_one_mem [Fintype α] (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 Preserves Universality when Identity is Present

Informal description

Let $\alpha$ be a finite type with a monoid structure. For any finite subset $s$ of $\alpha$ containing the multiplicative identity $1$, the pointwise product of $s$ with the universal finite set $\text{univ}$ (containing all elements of $\alpha$) is equal to $\text{univ}$, i.e., $s \cdot \text{univ} = \text{univ}$.

Finset.univ_mul_of_one_mem theorem

[Fintype α] (ht : (1 : α) ∈ t) : univ * t = univ

Full source

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

Universal set remains unchanged under pointwise multiplication with a set containing the identity

Informal description

Let $\alpha$ be a finite type with a monoid structure. For any finite subset $t$ of $\alpha$ containing the multiplicative identity $1$, the pointwise product of the universal finite set $\text{univ}$ (containing all elements of $\alpha$) with $t$ is equal to $\text{univ}$ itself, i.e., $\text{univ} \cdot t = \text{univ}$.

Finset.univ_mul_univ theorem

[Fintype α] : (univ : Finset α) * univ = univ

Full source

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

Universal Set is Closed Under Pointwise Multiplication

Informal description

For a finite type $\alpha$ equipped with a monoid structure, the pointwise multiplication of the universal finite set $\text{univ}$ (containing all elements of $\alpha$) with itself is equal to $\text{univ}$, i.e., $\text{univ} \cdot \text{univ} = \text{univ}$.

Finset.univ_pow theorem

[Fintype α] (hn : n ≠ 0) : (univ : Finset α) ^ n = univ

Full source

@[to_additive (attr := simp) nsmul_univ]
theorem univ_pow [Fintype α] (hn : n ≠ 0) : (univ : Finset α) ^ n = univ :=
  coe_injective <| by rw [coe_pow, coe_univ, Set.univ_pow hn]

Universal Finite Set is Closed Under Repeated Pointwise Multiplication: $\text{univ}^n = \text{univ}$ for $n \neq 0$

Informal description

For a finite type $\alpha$ equipped with a monoid structure and any nonzero natural number $n$, the $n$-th power of the universal finite set $\text{univ}$ (containing all elements of $\alpha$) under repeated pointwise multiplication is equal to $\text{univ}$ itself, i.e., $\text{univ}^n = \text{univ}$.

IsUnit.finset theorem

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

Full source

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

Singleton of a Unit is a Unit in Finite Sets

Informal description

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

Finset.image_op_pow theorem

(s : Finset α) : ∀ n : ℕ, (s ^ n).image op = s.image op ^ n

Full source

@[to_additive]
lemma image_op_pow (s : Finset α) : ∀ n : ℕ, (s ^ n).image op = s.image op ^ n
  | 0 => by simp [singleton_one]
  | n + 1 => by rw [pow_succ, pow_succ', image_op_mul, image_op_pow]

Image of Finite Set Power under Opposite Map Equals Power of Image

Informal description

For any finite subset $s$ of a type $\alpha$ and any natural number $n$, the image of the $n$-th power of $s$ under the canonical map $\text{op} : \alpha \to \alpha^\text{op}$ equals the $n$-th power of the image of $s$ under $\text{op}$ in the multiplicative opposite $\alpha^\text{op}$. That is: $$\text{op}(s^n) = (\text{op}(s))^n$$

Finset.map_op_pow theorem

(s : Finset α) : ∀ n : ℕ, (s ^ n).map opEquiv.toEmbedding = s.map opEquiv.toEmbedding ^ n

Full source

@[to_additive]
lemma map_op_pow (s : Finset α) :
    ∀ n : ℕ, (s ^ n).map opEquiv.toEmbedding = s.map opEquiv.toEmbedding ^ n
  | 0 => by simp [singleton_one]
  | n + 1 => by rw [pow_succ, pow_succ', map_op_mul, map_op_pow]

Power of Finite Set under Opposite Embedding: $\text{op}(s^n) = (\text{op}(s))^n$

Informal description

For any finite subset $s$ of a type $\alpha$ and any natural number $n$, the image of the $n$-th power of $s$ under the canonical embedding $\text{op} : \alpha \hookrightarrow \alpha^\text{op}$ equals the $n$-th power of the image of $s$ under $\text{op}$ in the multiplicative opposite $\alpha^\text{op}$. That is: $$\text{op}(s^n) = (\text{op}(s))^n$$

Finset.product_pow theorem

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

Full source

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

Power of Cartesian Product Equals Cartesian Product of Powers

Informal description

Let $s$ be a finite subset of a monoid $\alpha$ and $t$ a finite subset of a monoid $\beta$. 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$: $$(s \times t)^n = s^n \times t^n$$

Finset.commMonoid definition

: CommMonoid (Finset α)

Full source

/-- `Finset α` is a `CommMonoid` under pointwise operations if `α` is. -/
@[to_additive "`Finset α` is an `AddCommMonoid` under pointwise operations if `α` is. "]
protected def commMonoid : CommMonoid (Finset α) :=
  coe_injective.commMonoid _ coe_one coe_mul coe_pow

Commutative monoid structure on finite sets under pointwise operations

Informal description

The type of finite subsets `Finset α` of a commutative monoid `α` forms a commutative monoid under pointwise operations, where: - The multiplication of two finite sets `s` and `t` is the finite set `{x * y | x ∈ s, y ∈ t}`. - The multiplicative identity is the singleton set `{1}`. - The power operation `s^n` is defined as the repeated pointwise multiplication of `s` with itself `n` times.

Finset.coe_zpow theorem

(s : Finset α) : ∀ n : ℤ, ↑(s ^ n) = (s : Set α) ^ n

Full source

@[to_additive (attr := simp)]
theorem coe_zpow (s : Finset α) : ∀ n : ℤ, ↑(s ^ n) = (s : Set α) ^ n
  | Int.ofNat _ => coe_pow _ _
  | Int.negSucc n => by
    refine (coe_inv _).trans ?_
    exact congr_arg Inv.inv (coe_pow _ _)

Equality of Pointwise Integer Powers: $\overline{s^n} = \overline{s}^n$

Informal description

For any finite set $s$ of elements in a type $\alpha$ equipped with multiplication, inversion, and a multiplicative identity, and for any integer $n$, the underlying set of the $n$-th power of $s$ (defined by pointwise exponentiation) is equal to the $n$-th power of the underlying set of $s$. That is, $\overline{s^n} = \overline{s}^n$, where $\overline{\cdot}$ denotes the underlying set of a finite set and $(\cdot)^n$ denotes the pointwise exponentiation operation.

Finset.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
  simp_rw [← coe_inj, coe_mul, coe_one, Set.mul_eq_one_iff, coe_singleton]

Characterization of When Pointwise Product of Finite Sets is the Unit Singleton: $s * t = \{1\} \leftrightarrow \exists a b, s = \{a\} \wedge t = \{b\} \wedge a * b = 1$

Informal description

For finite sets $s$ and $t$ in a division monoid $\alpha$, the pointwise product $s * 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 * b = 1$.

Finset.divisionMonoid definition

: DivisionMonoid (Finset α)

Full source

/-- `Finset α` is a division monoid under pointwise operations if `α` is. -/
@[to_additive
  "`Finset α` is a subtraction monoid under pointwise operations if `α` is."]
protected def divisionMonoid : DivisionMonoid (Finset α) :=
  coe_injective.divisionMonoid _ coe_one coe_mul coe_inv coe_div coe_pow coe_zpow

Division monoid structure on finite sets via pointwise operations

Informal description

The type `Finset α` of finite subsets of a division monoid `α` forms a division monoid under pointwise operations. Specifically: - The multiplicative identity is the singleton `{1}`. - Multiplication is defined as `s * t = {x * y | x ∈ s, y ∈ t}`. - Inversion is defined as `s⁻¹ = {x⁻¹ | x ∈ s}`. - Division is defined as `s / t = {x / y | x ∈ s, y ∈ t}`. - Integer powers are defined as `sⁿ = {xⁿ | x ∈ s}` for `n ∈ ℤ`. This structure is inherited from `α` via the injective embedding of finite sets into sets, preserving all the division monoid operations.

Finset.isUnit_iff theorem

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

Full source

@[to_additive (attr := simp)]
theorem isUnit_iff : IsUnitIsUnit s ↔ ∃ a, s = {a} ∧ IsUnit a := by
  constructor
  · rintro ⟨u, rfl⟩
    obtain ⟨a, b, ha, hb, h⟩ := Finset.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.finset

Characterization of Units in Finite Sets: $s$ is a unit if and only if $s = \{a\}$ for some unit $a$

Informal description

A finite set $s$ in a division monoid $\alpha$ is a unit (i.e., has a multiplicative inverse) if and only if $s$ is a singleton $\{a\}$ for some unit element $a \in \alpha$.

Finset.isUnit_coe theorem

: IsUnit (s : Set α) ↔ IsUnit s

Full source

@[to_additive (attr := simp)]
theorem isUnit_coe : IsUnitIsUnit (s : Set α) ↔ IsUnit s := by
  simp_rw [isUnit_iff, Set.isUnit_iff, coe_eq_singleton]

Equivalence of Unit Conditions for Finite Sets and Their Set Embeddings

Informal description

For a finite set $s$ of elements in a monoid $\alpha$, the set $s$ (viewed as a subset of $\alpha$) is a unit in the monoid of sets if and only if $s$ is a unit in the monoid of finite sets under pointwise operations.

Finset.univ_div_univ theorem

[Fintype α] : (univ / univ : Finset α) = univ

Full source

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

Universal Finite Set is Closed Under Pointwise Division

Informal description

For a finite type $\alpha$ equipped with a division operation, the pointwise division of the universal finite set (containing all elements of $\alpha$) by itself is equal to the universal finite set, i.e., $\text{univ} / \text{univ} = \text{univ}$.

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

Left Subset Property of Pointwise Division with Identity

Informal description

For any finite sets $s$ and $t$ in a division monoid $\alpha$, if the multiplicative identity $1$ belongs to $t$, then $s$ is a subset of the pointwise division $s / t$.

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

Inclusion of Inverses in Division by Identity-Containing Set

Informal description

For any finite sets $s$ and $t$ in a division monoid $\alpha$, if $s$ contains the multiplicative identity $1$, then the pointwise inverse of $t$ is a subset of the pointwise division $s / t$. That is, $t^{-1} \subseteq s / t$.

Finset.empty_zpow theorem

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

Full source

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

Empty Finset Integer Power Law: $\emptyset^n = \emptyset$ for $n \neq 0$

Informal description

For any integer $n \neq 0$, the $n$-th power of the empty finset $\emptyset$ under pointwise operations is the empty finset, i.e., $\emptyset^n = \emptyset$.

Finset.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 Finite Sets Remain Nonempty Under Integer Powers

Informal description

For any nonempty finite set $s$ in a division monoid $\alpha$ and any integer $n$, the $n$-th power of $s$ under pointwise multiplication is nonempty.

Finset.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 nonempty_iff_ne_empty.1 (nonempty_iff_ne_empty.2 hs).zpow
    · rw [← nonempty_iff_ne_empty]
      simp
  · rintro ⟨rfl, hn⟩
    exact empty_zpow hn

Characterization of Empty Finset Powers: $s^n = \emptyset \iff (s = \emptyset \land n \neq 0)$

Informal description

For any finite set $s$ in a division monoid $\alpha$ and any integer $n$, the $n$-th power of $s$ under pointwise operations is empty if and only if $s$ is empty and $n$ is nonzero.

Finset.singleton_zpow theorem

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

Full source

@[to_additive (attr := simp) zsmul_singleton]
lemma singleton_zpow (a : α) (n : ℤ) : ({a} : Finset α) ^ 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$ with a multiplicative identity, multiplication, and inversion operations, and for any integer $n$, the integer power of the singleton set $\{a\}$ under pointwise operations equals the singleton set $\{a^n\}$, where $a^n$ denotes the $n$-th power of $a$ in $\alpha$.

Finset.divisionCommMonoid definition

[DivisionCommMonoid α] : DivisionCommMonoid (Finset α)

Full source

/-- `Finset α` is a commutative division monoid under pointwise operations if `α` is. -/
@[to_additive subtractionCommMonoid
      "`Finset α` is a commutative subtraction monoid under pointwise operations if `α` is."]
protected def divisionCommMonoid [DivisionCommMonoid α] : DivisionCommMonoid (Finset α) :=
  coe_injective.divisionCommMonoid _ coe_one coe_mul coe_inv coe_div coe_pow coe_zpow

Commutative division monoid structure on finite sets via pointwise operations

Informal description

For a type $\alpha$ that is a commutative division monoid, the type `Finset α` of finite subsets of $\alpha$ inherits a commutative division monoid structure under pointwise operations. Specifically: - The multiplication of two finite sets $s$ and $t$ is defined as $\{x \cdot y \mid x \in s, y \in t\}$. - The inversion of a finite set $s$ is defined as $\{x^{-1} \mid x \in s\}$. - The division of two finite sets $s$ and $t$ is defined as $\{x / y \mid x \in s, y \in t\}$. - The multiplicative identity is the singleton $\{1\}$. This structure is obtained by lifting the operations from $\alpha$ to `Finset α` via the injective coercion map from finite sets to sets.

Finset.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
  rw [← mem_coe, ← disjoint_coe, coe_div, Set.one_mem_div_iff]

Characterization of Non-Disjoint Finite Sets via Pointwise Division: $1 \in s / t \leftrightarrow s \cap t \neq \emptyset$

Informal description

For finite 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., $s \cap t \neq \emptyset$).

Finset.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,
    Finset.Nonempty])

Characterization of Non-Disjoint Finite Sets via Pointwise Inversion and Multiplication: $1 \in t^{-1} * s \leftrightarrow s \cap t \neq \emptyset$

Informal description

For finite sets $s$ and $t$ in a group $\alpha$, the multiplicative identity $1$ is an element of the pointwise product $t^{-1} * s$ if and only if $s$ and $t$ are not disjoint (i.e., they have a common element).

Finset.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 Finite Sets via Pointwise Division: $1 \notin s / t \leftrightarrow s \cap t = \emptyset$

Informal description

For finite 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$).

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

Characterization of Disjoint Finite Sets via Pointwise Inversion and Multiplication: $1 \notin t^{-1} * s \leftrightarrow s \cap t = \emptyset$

Informal description

For finite 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$).

Finset.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 Pointwise Division of Nonempty Finite Sets

Informal description

For any nonempty finite set $s$ in a group $\alpha$, the identity element $1$ is contained in the pointwise division $s / s$, where $s / s$ is the set $\{x / y \mid x, y \in s\}$.

Finset.isUnit_singleton theorem

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

Full source

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

Singleton Finite Sets are Units in Pointwise Monoid

Informal description

For any element $a$ in a monoid $\alpha$, the singleton finite set $\{a\}$ is a unit (i.e., invertible under pointwise multiplication) in the monoid of finite subsets of $\alpha$.

Finset.isUnit_iff_singleton theorem

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

Full source

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

Characterization of Unit Finite Sets as Singletons in a Monoid

Informal description

A finite set $s$ in a monoid $\alpha$ is a unit (i.e., invertible under pointwise multiplication) if and only if $s$ is a singleton set $\{a\}$ for some element $a \in \alpha$.

Finset.isUnit_iff_singleton_aux theorem

{α} [Group α] {s : Finset α} : (∃ a, s = { a } ∧ IsUnit a) ↔ ∃ a, s = { a }

Full source

@[simp]
theorem isUnit_iff_singleton_aux {α} [Group α] {s : Finset α} :
    (∃ a, s = {a} ∧ IsUnit a) ↔ ∃ a, s = {a} := by
  simp only [Group.isUnit, and_true]

Characterization of Singleton Finite Sets Containing Units in a Group

Informal description

For a finite set $s$ in a group $\alpha$, the following are equivalent: 1. There exists an element $a \in \alpha$ such that $s = \{a\}$ and $a$ is a unit (i.e., invertible). 2. There exists an element $a \in \alpha$ such that $s = \{a\}$.

Finset.image_mul_left theorem

: image (fun b => a * b) t = preimage t (fun b => a⁻¹ * b) (mul_right_injective _).injOn

Full source

@[to_additive (attr := simp)]
theorem image_mul_left :
    image (fun b => a * b) t = preimage t (fun b => a⁻¹ * b) (mul_right_injective _).injOn :=
  coe_injective <| by simp

Image under Left Multiplication Equals Preimage under Inverse Left Multiplication in Finite Sets

Informal description

For any element $a$ in a group $\alpha$ and any finite subset $t \subseteq \alpha$, the image of $t$ under left multiplication by $a$ is equal to the preimage of $t$ under left multiplication by $a^{-1}$. That is, $$ \{a \cdot b \mid b \in t\} = \{c \mid a^{-1} \cdot c \in t\}. $$

Finset.image_mul_right theorem

: image (· * b) t = preimage t (· * b⁻¹) (mul_left_injective _).injOn

Full source

@[to_additive (attr := simp)]
theorem image_mul_right : image (· * b) t = preimage t (· * b⁻¹) (mul_left_injective _).injOn :=
  coe_injective <| by simp

Right Multiplication Image Equals Preimage under Inverse in Finite Sets

Informal description

For any element $b$ in a group $\alpha$ and any finite subset $t \subseteq \alpha$, the image of $t$ under right multiplication by $b$ equals the preimage of $t$ under right multiplication by $b^{-1}$. That is, $$ \{x \cdot b \mid x \in t\} = \{y \mid y \cdot b^{-1} \in t\}. $$

Finset.image_mul_left' theorem

: image (fun b => a⁻¹ * b) t = preimage t (fun b => a * b) (mul_right_injective _).injOn

Full source

@[to_additive]
theorem image_mul_left' :
    image (fun b => a⁻¹ * b) t = preimage t (fun b => a * b) (mul_right_injective _).injOn := by
  simp

Image under Inverse Left Multiplication Equals Preimage under Left Multiplication in Finite Sets

Informal description

For any element $a$ in a group $\alpha$ and any finite subset $t \subseteq \alpha$, the image of $t$ under left multiplication by $a^{-1}$ is equal to the preimage of $t$ under left multiplication by $a$. That is, $$ \{a^{-1} \cdot b \mid b \in t\} = \{c \mid a \cdot c \in t\}. $$

Finset.image_mul_right' theorem

: image (· * b⁻¹) t = preimage t (· * b) (mul_left_injective _).injOn

Full source

@[to_additive]
theorem image_mul_right' :
    image (· * b⁻¹) t = preimage t (· * b) (mul_left_injective _).injOn := by simp

Right Multiplication by Inverse Equals Preimage under Original Element in Finite Sets

Informal description

For any element $b$ in a group $\alpha$ and any finite subset $t \subseteq \alpha$, the image of $t$ under right multiplication by $b^{-1}$ equals the preimage of $t$ under right multiplication by $b$. That is, $$ \{x \cdot b^{-1} \mid x \in t\} = \{y \mid y \cdot b \in t\}. $$

Finset.image_inv theorem

(f : F) (s : Finset α) : s⁻¹.image f = (s.image f)⁻¹

Full source

@[to_additive]
lemma image_inv (f : F) (s : Finset α) : s⁻¹.image f = (s.image f)⁻¹ := image_comm (map_inv _)

Monoid Homomorphism Preserves Pointwise Inversion: $f[s^{-1}] = (f[s])^{-1}$

Informal description

Let $F$ be a type of homomorphisms between monoids, and let $f \in F$ be a monoid homomorphism. For any finite set $s$ of elements in a monoid $\alpha$, the image of the pointwise inverse of $s$ under $f$ is equal to the pointwise inverse of the image of $s$ under $f$. That is, $$ f[s^{-1}] = (f[s])^{-1}, $$ where $s^{-1} = \{x^{-1} \mid x \in s\}$ and $f[s] = \{f(x) \mid x \in s\}$.

Finset.image_div theorem

: (s / t).image (f : α → β) = s.image f / t.image f

Full source

theorem image_div : (s / t).image (f : α → β) = s.image f / t.image f :=
  image_image₂_distrib <| map_div f

Image of Pointwise Division Equals Pointwise Division of Images: $f(s / t) = f(s) / f(t)$

Informal description

For any finite sets $s$ and $t$ of type $\alpha$ and any function $f \colon \alpha \to \beta$ (where $\beta$ has a division operation), the image of the pointwise division set $s / t$ under $f$ equals the pointwise division of the images $f(s)$ and $f(t)$. That is, $$ f(s / t) = f(s) / f(t), $$ where $s / t = \{x / y \mid x \in s, y \in t\}$ and $f(s) = \{f(x) \mid x \in s\}$.

Finset.preimage_mul_left_singleton theorem

: preimage { b } (a * ·) (mul_right_injective _).injOn = {a⁻¹ * b}

Full source

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

Preimage of Singleton under Left Multiplication in a Group: $\{a^{-1} \cdot b\}$

Informal description

For any element $a$ in a group $\alpha$ and any singleton set $\{b\}$ where $b \in \alpha$, the preimage of $\{b\}$ under the left multiplication map $x \mapsto a \cdot x$ is the singleton set $\{a^{-1} \cdot b\}$.

Finset.preimage_mul_right_singleton theorem

: preimage { b } (· * a) (mul_left_injective _).injOn = {b * a⁻¹}

Full source

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

Preimage of Singleton under Right Multiplication: $\{b \cdot a^{-1}\}$

Informal description

For any elements $a$ and $b$ in a group $\alpha$, the preimage of the singleton set $\{b\}$ under the right multiplication map $x \mapsto x \cdot a$ is the singleton set $\{b \cdot a^{-1}\}$.

Finset.preimage_mul_left_one theorem

: preimage 1 (a * ·) (mul_right_injective _).injOn = {a⁻¹}

Full source

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

Preimage of identity under left multiplication: $\{a^{-1}\}$

Informal description

For any element $a$ in a group $\alpha$, the preimage of the singleton set $\{1\}$ under the left multiplication map $x \mapsto a \cdot x$ is the singleton set $\{a^{-1}\}$.

Finset.preimage_mul_right_one theorem

: preimage 1 (· * b) (mul_left_injective _).injOn = {b⁻¹}

Full source

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

Preimage of Identity under Right Multiplication is Singleton Inverse

Informal description

For any element $b$ in a group $\alpha$, the preimage of the singleton finset $\{1\}$ under the right multiplication map $x \mapsto x \cdot b$ is the singleton finset $\{b^{-1}\}$. That is, $$ \{x \mid x \cdot b = 1\} = \{b^{-1}\}. $$

Finset.preimage_mul_left_one' theorem

: preimage 1 (a⁻¹ * ·) (mul_right_injective _).injOn = { a }

Full source

@[to_additive]
theorem preimage_mul_left_one' : preimage 1 (a⁻¹ * ·) (mul_right_injective _).injOn = {a} := by
  rw [preimage_mul_left_one, inv_inv]

Preimage of identity under left multiplication by inverse: $\{a\}$

Informal description

For any element $a$ in a group $\alpha$, the preimage of the singleton set $\{1\}$ under the left multiplication map $x \mapsto a^{-1} \cdot x$ is the singleton set $\{a\}$.

Finset.preimage_mul_right_one' theorem

: preimage 1 (· * b⁻¹) (mul_left_injective _).injOn = { b }

Full source

@[to_additive]
theorem preimage_mul_right_one' : preimage 1 (· * b⁻¹) (mul_left_injective _).injOn = {b} := by
  rw [preimage_mul_right_one, inv_inv]

Preimage of Identity under Right Multiplication by Inverse is Singleton Element

Informal description

For any element $b$ in a group $\alpha$, the preimage of the singleton finset $\{1\}$ under the right multiplication map $x \mapsto x \cdot b^{-1}$ is the singleton finset $\{b\}$. That is, $$ \{x \mid x \cdot b^{-1} = 1\} = \{b\}. $$

Finset.image_pow_of_ne_zero theorem

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

Full source

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

Image of Finite Set Power under Homomorphism Equals Power of Image for Nonzero Exponents

Informal description

Let $\alpha$ and $\beta$ be types, and let $F$ be a type of homomorphisms between multiplicative structures $\alpha$ and $\beta$. For any natural number $n \neq 0$, any homomorphism $f \in F$, and any finite subset $s \subseteq \alpha$, 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 $$

Finset.image_pow theorem

[MonoidHomClass F α β] (f : F) (s : Finset α) : ∀ n, (s ^ n).image f = s.image f ^ n

Full source

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

Image of Finite Set Power under Monoid Homomorphism Equals Power of Image

Informal description

Let $\alpha$ and $\beta$ be monoids, and let $F$ be a type of monoid homomorphisms from $\alpha$ to $\beta$. For any monoid homomorphism $f \in F$, any finite 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 $$

Finset.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 Left Multiplication of Finite Sets: $t$ nontrivial and $s$ nonempty implies $s * t$ nontrivial

Informal description

Let $s$ and $t$ be finite sets in a type $\alpha$ with multiplication. 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 * t$ is nontrivial.

Finset.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 Finite Sets

Informal description

For any finite sets $s$ and $t$ in a type $\alpha$ with multiplication, if both $s$ and $t$ are nontrivial (i.e., each contains at least two distinct elements), then their pointwise product $s * t$ is also nontrivial.

Finset.card_singleton_mul theorem

(a : α) (t : Finset α) : #({ a } * t) = #t

Full source

@[to_additive (attr := simp)]
theorem card_singleton_mul (a : α) (t : Finset α) : #({a} * t) = #t :=
  card_image₂_singleton_left _ <| mul_right_injective _

Cardinality of Singleton Multiplication: $\#(\{a\} * t) = \#t$

Informal description

For any element $a$ in a type $\alpha$ and any finite set $t \subseteq \alpha$, the cardinality of the pointwise product $\{a\} * t$ equals the cardinality of $t$. Here, $\{a\} * t$ denotes the set $\{a \cdot x \mid x \in t\}$.

Finset.singleton_mul_inter theorem

(a : α) (s t : Finset α) : { a } * (s ∩ t) = { a } * s ∩ ({ a } * t)

Full source

@[to_additive]
theorem singleton_mul_inter (a : α) (s t : Finset α) : {a} * (s ∩ t) = {a}{a} * s ∩ ({a} * t) :=
  image₂_singleton_inter _ _ <| mul_right_injective _

Distributivity of Singleton Multiplication over Intersection: $\{a\} * (s \cap t) = (\{a\} * s) \cap (\{a\} * t)$

Informal description

For any element $a$ in a type $\alpha$ and any finite sets $s, t \subseteq \alpha$, the pointwise product of the singleton set $\{a\}$ with the intersection $s \cap t$ equals the intersection of the pointwise products $\{a\} * s$ and $\{a\} * t$. That is, \[ \{a\} * (s \cap t) = (\{a\} * s) \cap (\{a\} * t). \]

Finset.card_le_card_mul_left theorem

{s : Finset α} (hs : s.Nonempty) : #t ≤ #(s * t)

Full source

@[to_additive]
theorem card_le_card_mul_left {s : Finset α} (hs : s.Nonempty) : #t ≤ #(s * t) :=
  card_le_card_image₂_left _ hs mul_right_injective

Cardinality inequality: $\#t \leq \#(s * t)$ for nonempty $s$ under left-cancellative multiplication

Informal description

For any nonempty finite set $s$ and any finite set $t$ in a type $\alpha$ with left-cancellative multiplication, the cardinality of $t$ is less than or equal to the cardinality of the pointwise product set $s * t$.

Finset.card_le_card_mul_self theorem

{s : Finset α} : #s ≤ #(s * s)

Full source

/--
The size of `s * s` is at least the size of `s`, version with left-cancellative multiplication.
See `card_le_card_mul_self'` for the version with right-cancellative multiplication.
-/
@[to_additive
"The size of `s + s` is at least the size of `s`, version with left-cancellative addition.
See `card_le_card_add_self'` for the version with right-cancellative addition."]
theorem card_le_card_mul_self {s : Finset α} : #s ≤ #(s * s) := by
  cases s.eq_empty_or_nonempty <;> simp [card_le_card_mul_left, *]

Cardinality inequality for pointwise product: $\#s \leq \#(s * s)$ under left-cancellative multiplication

Informal description

For any finite set $s$ of elements in a type $\alpha$ with a left-cancellative multiplication operation, the cardinality of $s$ is less than or equal to the cardinality of the pointwise product set $s * s$.

Finset.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: $s$ nontrivial and $t$ nonempty implies $s * t$ nontrivial

Informal description

For any finite sets $s$ and $t$ of a type $\alpha$ with multiplication, if $s$ is nontrivial (contains at least two distinct elements) and $t$ is nonempty (contains at least one element), then the pointwise product set $s * t$ is also nontrivial.

Finset.card_mul_singleton theorem

(s : Finset α) (a : α) : #(s * { a }) = #s

Full source

@[to_additive (attr := simp)]
theorem card_mul_singleton (s : Finset α) (a : α) : #(s * {a}) = #s :=
  card_image₂_singleton_right _ <| mul_left_injective _

Cardinality of Pointwise Product with Singleton: $\#(s * \{a\}) = \#s$

Informal description

For any finite set $s$ of type $\alpha$ and any element $a \in \alpha$, the cardinality of the pointwise product $s * \{a\}$ equals the cardinality of $s$.

Finset.inter_mul_singleton theorem

(s t : Finset α) (a : α) : s ∩ t * { a } = s * { a } ∩ (t * { a })

Full source

@[to_additive]
theorem inter_mul_singleton (s t : Finset α) (a : α) : s ∩ t * {a} = s * {a} ∩ (t * {a}) :=
  image₂_inter_singleton _ _ <| mul_left_injective _

Intersection-Preserving Property of Pointwise Multiplication with Singleton: $(s \cap t) * \{a\} = (s * \{a\}) \cap (t * \{a\})$

Informal description

For any finite sets $s$ and $t$ of a type $\alpha$ with multiplication, and for any element $a \in \alpha$, the pointwise product of the intersection $s \cap t$ with the singleton $\{a\}$ equals the intersection of the pointwise products $s * \{a\}$ and $t * \{a\}$, i.e., \[ (s \cap t) * \{a\} = (s * \{a\}) \cap (t * \{a\}). \]

Finset.card_le_card_mul_right theorem

(ht : t.Nonempty) : #s ≤ #(s * t)

Full source

@[to_additive]
theorem card_le_card_mul_right (ht : t.Nonempty) : #s ≤ #(s * t) :=
  card_le_card_image₂_right _ ht mul_left_injective

Cardinality Lower Bound for Pointwise Product with Nonempty Set: $\#s \leq \#(s * t)$

Informal description

For any nonempty finite set $t$ and any finite set $s$, the cardinality of $s$ is less than or equal to the cardinality of their pointwise product $s * t$, i.e., $\#s \leq \#(s * t)$.

Finset.card_le_card_mul_self' theorem

: #s ≤ #(s * s)

Full source

/--
The size of `s * s` is at least the size of `s`, version with right-cancellative multiplication.
See `card_le_card_mul_self` for the version with left-cancellative multiplication.
-/
@[to_additive
"The size of `s + s` is at least the size of `s`, version with right-cancellative addition.
See `card_le_card_add_self` for the version with left-cancellative addition."]
theorem card_le_card_mul_self' : #s ≤ #(s * s) := by
  cases s.eq_empty_or_nonempty <;> simp [card_le_card_mul_right, *]

Cardinality Bound for Pointwise Square under Right-Cancellative Multiplication

Informal description

For any finite set $s$ with a right-cancellative multiplication operation, the cardinality of $s$ is less than or equal to the cardinality of the pointwise product $s * s$, i.e., $\#s \leq \#(s * s)$.

Finset.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 Powers of Nontrivial Finite Sets: $(s^n).\text{Nontrivial}$ for $n \neq 0$

Informal description

For any nontrivial finite set $s$ (i.e., containing at least two distinct elements) in a monoid, and for any nonzero natural number $n$, the $n$-th power of $s$ under pointwise multiplication is also nontrivial.

Finset.Nonempty.card_pow_mono theorem

(hs : s.Nonempty) : Monotone fun n : ℕ ↦ #(s ^ n)

Full source

/-- See `Finset.card_pow_mono` for a version that works for the empty set. -/
@[to_additive "See `Finset.card_nsmul_mono` for a version that works for the empty set."]
protected lemma Nonempty.card_pow_mono (hs : s.Nonempty) : Monotone fun n : ℕ ↦ #(s ^ n) :=
  monotone_nat_of_le_succ fun n ↦ by rw [pow_succ]; exact card_le_card_mul_right hs

Monotonicity of Cardinality under Powers of Nonempty Finite Sets: $\#(s^m) \leq \#(s^n)$ for $m \leq n$

Informal description

For any nonempty finite set $s$ in a monoid, the function $n \mapsto \#(s^n)$ is monotone with respect to the natural number ordering. That is, for any natural numbers $m \leq n$, the cardinality of the $m$-th power of $s$ is less than or equal to the cardinality of the $n$-th power of $s$.

Finset.card_pow_mono theorem

(hm : m ≠ 0) (hmn : m ≤ n) : #(s ^ m) ≤ #(s ^ n)

Full source

/-- See `Finset.Nonempty.card_pow_mono` for a version that works for zero powers. -/
@[to_additive "See `Finset.Nonempty.card_nsmul_mono` for a version that works for zero scalars."]
lemma card_pow_mono (hm : m ≠ 0) (hmn : m ≤ n) : #(s ^ m) ≤ #(s ^ n) := by
  obtain rfl | hs := s.eq_empty_or_nonempty
  · simp [hm]
  · exact hs.card_pow_mono hmn

Monotonicity of Cardinality under Powers: $\#(s^m) \leq \#(s^n)$ for $0 < m \leq n$

Informal description

For any finite set $s$ in a monoid and natural numbers $m$ and $n$ such that $m \neq 0$ and $m \leq n$, the cardinality of the $m$-th power of $s$ is less than or equal to the cardinality of the $n$-th power of $s$, i.e., $\#(s^m) \leq \#(s^n)$.

Finset.card_le_card_pow theorem

(hn : n ≠ 0) : #s ≤ #(s ^ n)

Full source

@[to_additive]
lemma card_le_card_pow (hn : n ≠ 0) : #s ≤ #(s ^ n) := by
  simpa using card_pow_mono (s := s) one_ne_zero (Nat.one_le_iff_ne_zero.2 hn)

Cardinality Inequality for Finite Set Powers: $\#s \leq \#(s^n)$ when $n \neq 0$

Informal description

For any finite set $s$ in a monoid and any nonzero natural number $n$, the cardinality of $s$ is less than or equal to the cardinality of the $n$-th power of $s$, i.e., $\#s \leq \#(s^n)$.

Finset.card_le_card_div_left theorem

(hs : s.Nonempty) : #t ≤ #(s / t)

Full source

@[to_additive] lemma card_le_card_div_left (hs : s.Nonempty) : #t ≤ #(s / t) :=
  card_le_card_image₂_left _ hs fun _ ↦ div_right_injective

Cardinality inequality: $\#t \leq \#(s / t)$ for nonempty $s$

Informal description

For any nonempty finite set $s$ and any finite set $t$ in a type $\alpha$ equipped with a division operation, the cardinality of $t$ is less than or equal to the cardinality of the pointwise division $s / t$ (where $s / t := \{x / y \mid x \in s, y \in t\}$).

Finset.card_le_card_div_right theorem

(ht : t.Nonempty) : #s ≤ #(s / t)

Full source

@[to_additive] lemma card_le_card_div_right (ht : t.Nonempty) : #s ≤ #(s / t) :=
  card_le_card_image₂_right _ ht fun _ ↦ div_left_injective

Cardinality inequality: $\#s \leq \#(s / t)$ for nonempty $t$

Informal description

For any nonempty finite set $t$ and any finite set $s$ in a type $\alpha$ equipped with a division operation, the cardinality of $s$ is less than or equal to the cardinality of the pointwise division $s / t := \{x / y \mid x \in s, y \in t\}$.

Finset.card_le_card_div_self theorem

: #s ≤ #(s / s)

Full source

@[to_additive] lemma card_le_card_div_self : #s ≤ #(s / s) := by
  cases s.eq_empty_or_nonempty <;> simp [card_le_card_div_left, *]

Cardinality Inequality for Self-Division of Finite Sets: $\#s \leq \#(s / s)$

Informal description

For any finite set $s$ of a type $\alpha$ equipped with a division operation, the cardinality of $s$ is less than or equal to the cardinality of the pointwise division of $s$ by itself, i.e., $\#s \leq \#(s / s)$.

Fintype.piFinset_mul theorem

[∀ i, Mul (α i)] (s t : ∀ i, Finset (α i)) : piFinset (fun i ↦ s i * t i) = piFinset s * piFinset t

Full source

@[to_additive]
lemma piFinset_mul [∀ i, Mul (α i)] (s t : ∀ i, Finset (α i)) :
    piFinset (fun i ↦ s i * t i) = piFinset s * piFinset t := piFinset_image₂ _ _ _

Finite Product Commutes with Pointwise Multiplication

Informal description

For a finite type $I$ and a family of types $(\alpha_i)_{i \in I}$ each equipped with a multiplication operation, the finite product set $\prod_{i \in I} (s_i * t_i)$ (where each $s_i$ and $t_i$ are finite subsets of $\alpha_i$) is equal to the pointwise product of the finite product sets $\left(\prod_{i \in I} s_i\right) * \left(\prod_{i \in I} t_i\right)$. In other words, $\prod_{i \in I} (s_i * t_i) = \left(\prod_{i \in I} s_i\right) * \left(\prod_{i \in I} t_i\right)$.

Fintype.piFinset_div theorem

[∀ i, Div (α i)] (s t : ∀ i, Finset (α i)) : piFinset (fun i ↦ s i / t i) = piFinset s / piFinset t

Full source

@[to_additive]
lemma piFinset_div [∀ i, Div (α i)] (s t : ∀ i, Finset (α i)) :
    piFinset (fun i ↦ s i / t i) = piFinset s / piFinset t := piFinset_image₂ _ _ _

Finite Product Commutes with Pointwise Division: $\prod_i (s_i / t_i) = (\prod_i s_i) / (\prod_i t_i)$

Informal description

For a finite type $I$ and a family of types $(\alpha_i)_{i \in I}$ each equipped with a division operation, the finite product of pointwise divisions $\prod_{i \in I} (s_i / t_i)$ is equal to the pointwise division of the finite products $(\prod_{i \in I} s_i) / (\prod_{i \in I} t_i)$, where $s_i$ and $t_i$ are finite subsets of $\alpha_i$ for each $i \in I$.

Fintype.piFinset_inv theorem

[∀ i, Inv (α i)] (s : ∀ i, Finset (α i)) : piFinset (fun i ↦ (s i)⁻¹) = (piFinset s)⁻¹

Full source

@[to_additive (attr := simp)]
lemma piFinset_inv [∀ i, Inv (α i)] (s : ∀ i, Finset (α i)) :
    piFinset (fun i ↦ (s i)⁻¹) = (piFinset s)⁻¹ := piFinset_image _ _

Pointwise Inversion Commutes with Finite Product of Finite Sets

Informal description

For a finite type $I$ and a family of types $(\alpha_i)_{i \in I}$ each equipped with an inversion operation, the pointwise inversion of the finite product set $\prod_{i \in I} s_i$ (where each $s_i$ is a finite subset of $\alpha_i$) is equal to the finite product set of the pointwise inverses $\prod_{i \in I} s_i^{-1}$. In other words, $\left(\prod_{i \in I} s_i\right)^{-1} = \prod_{i \in I} s_i^{-1}$.

Set.instFintypeOne instance

[One α] : Fintype (1 : Set α)

Full source

@[to_additive]
instance instFintypeOne [One α] : Fintype (1 : Set α) := Set.fintypeSingleton _

Finiteness of the Singleton Set Containing One

Informal description

For any type $\alpha$ with a distinguished element $1$, the singleton set $\{1\}$ is finite.

Set.toFinset_one theorem

: (1 : Set α).toFinset = 1

Full source

@[to_additive (attr := simp)]
theorem toFinset_one : (1 : Set α).toFinset = 1 :=
  rfl

Conversion of Singleton Set $\{1\}$ to Finset Yields $1$

Informal description

The finite set obtained by converting the singleton set $\{1\}$ (where $1$ is the multiplicative identity of type $\alpha$) is equal to the singleton finset $1$.

Set.toFinset_mul theorem

(s t : Set α) [Fintype s] [Fintype t] [Fintype ↑(s * t)] : (s * t).toFinset = s.toFinset * t.toFinset

Full source

@[to_additive (attr := simp)]
theorem toFinset_mul (s t : Set α) [Fintype s] [Fintype t] [Fintype ↑(s * t)] :
    (s * t).toFinset = s.toFinset * t.toFinset :=
  toFinset_image2 _ _ _

Equality of Pointwise Product Conversions: $(s * t).\text{toFinset} = s.\text{toFinset} * t.\text{toFinset}$

Informal description

For any finite sets $s, t \subseteq \alpha$ (with `Fintype` instances for $s$, $t$, and $s * t$), the finite set obtained by converting the pointwise product set $s * t = \{x * y \mid x \in s, y \in t\}$ to a `Finset` is equal to the pointwise product of the finite sets $s.\text{toFinset}$ and $t.\text{toFinset}$.

Mathlib.Algebra.Group.Pointwise.Finset.Basic

Main declarations

Implementation notes

Tags