Mathlib.Algebra.Order.Group.Finset

Multiset.toFinset_nsmul theorem

(s : Multiset α) : ∀ n ≠ 0, (n • s).toFinset = s.toFinset

Full source

@[simp] lemma toFinset_nsmul (s : Multiset α) : ∀ n ≠ 0, (n • s).toFinset = s.toFinset
  | 0, h => by contradiction
  | n + 1, _ => by
    by_cases h : n = 0
    · rw [h, zero_add, one_nsmul]
    · rw [add_nsmul, toFinset_add, one_nsmul, toFinset_nsmul s n h, Finset.union_idempotent]

Scalar Multiplication Preserves Support of Multiset

Informal description

For any multiset $s$ over a type $\alpha$ and any nonzero natural number $n$, the finite set corresponding to the scalar multiple $n \cdot s$ is equal to the finite set corresponding to $s$, i.e., $(n \cdot s).\text{toFinset} = s.\text{toFinset}$.

Multiset.toFinset_eq_singleton_iff theorem

(s : Multiset α) (a : α) : s.toFinset = { a } ↔ card s ≠ 0 ∧ s = card s • { a }

Full source

lemma toFinset_eq_singleton_iff (s : Multiset α) (a : α) :
    s.toFinset = {a} ↔ card s ≠ 0 ∧ s = card s • {a} := by
  refine ⟨fun H ↦ ⟨fun h ↦ ?_, ext' fun x ↦ ?_⟩, fun H ↦ ?_⟩
  · rw [card_eq_zero.1 h, toFinset_zero] at H
    exact Finset.singleton_ne_empty _ H.symm
  · rw [count_nsmul, count_singleton]
    by_cases hx : x = a
    · simp_rw [hx, ite_true, mul_one, count_eq_card]
      intro y hy
      rw [← mem_toFinset, H, Finset.mem_singleton] at hy
      exact hy.symm
    have hx' : x ∉ s := fun h' ↦ hx <| by rwa [← mem_toFinset, H, Finset.mem_singleton] at h'
    simp_rw [count_eq_zero_of_not_mem hx', hx, ite_false, Nat.mul_zero]
  simpa only [toFinset_nsmul _ _ H.1, toFinset_singleton] using congr($(H.2).toFinset)

Characterization of Multisets with Singleton Support: $s.\text{toFinset} = \{a\} \leftrightarrow |s| \neq 0 \land s = |s| \cdot \{a\}$

Informal description

For any multiset $s$ over a type $\alpha$ and any element $a \in \alpha$, the finite set corresponding to $s$ is the singleton $\{a\}$ if and only if $s$ is non-empty and $s$ consists of $n$ copies of $a$, where $n$ is the cardinality of $s$. In other words: $$s.\text{toFinset} = \{a\} \leftrightarrow |s| \neq 0 \land s = |s| \cdot \{a\}.$$

Multiset.toFinset_card_eq_one_iff theorem

(s : Multiset α) : #s.toFinset = 1 ↔ Multiset.card s ≠ 0 ∧ ∃ a : α, s = Multiset.card s • { a }

Full source

lemma toFinset_card_eq_one_iff (s : Multiset α) :
    #s.toFinset#s.toFinset = 1 ↔ Multiset.card s ≠ 0 ∧ ∃ a : α, s = Multiset.card s • {a} := by
  simp_rw [Finset.card_eq_one, Multiset.toFinset_eq_singleton_iff, exists_and_left]

Characterization of Multisets with Singleton Support

Informal description

For any multiset $s$ over a type $\alpha$, the cardinality of the corresponding finset is equal to 1 if and only if $s$ is non-empty and there exists an element $a \in \alpha$ such that $s$ consists of $n$ copies of $a$, where $n$ is the cardinality of $s$. In other words: $$|s.\text{toFinset}| = 1 \leftrightarrow s \neq \emptyset \land \exists a \in \alpha, s = n \cdot \{a\} \text{ where } n = |s|$$

Finset.fold_max_add theorem

 [LinearOrder M] [Add M] [AddRightMono M] (s : Finset ι) (a : WithBot M) (f : ι → M) :
  s.fold max ⊥ (fun i ↦ ↑(f i) + a) = s.fold max ⊥ ((↑) ∘ f) + a

Full source

lemma fold_max_add [LinearOrder M] [Add M] [AddRightMono M] (s : Finset ι) (a : WithBot M)
    (f : ι → M) : s.fold max ⊥ (fun i ↦ ↑(f i) + a) = s.fold max ⊥ ((↑) ∘ f) + a := by
  classical
    induction' s using Finset.induction_on with a s _ ih <;> simp [*, max_add_add_right]

Right-Monotone Additivity of Max-Fold over Finite Sets: $\text{fold max } \bot (f + a) = (\text{fold max } \bot f) + a$

Informal description

Let $M$ be a linearly ordered additive monoid where addition is right-monotone (i.e., $x \leq y$ implies $x + z \leq y + z$ for all $z$). For any finite set $s$ indexed by $\iota$, any element $a \in \text{WithBot}\, M$, and any function $f : \iota \to M$, the following equality holds: $$\text{fold max } \bot \text{ over } s \text{ of } (f(i) + a) = \left(\text{fold max } \bot \text{ over } s \text{ of } f(i)\right) + a.$$ Here, $\text{WithBot}\, M$ denotes $M$ with an adjoined bottom element $\bot$, and $\text{fold}$ is the standard fold operation over the finite set $s$ with the binary operation $\max$ and initial value $\bot$.

Finset.inf'_pow theorem

 [LinearOrder M] [Monoid M] [MulLeftMono M] [MulRightMono M] (s : Finset ι) (f : ι → M) (n : ℕ) (hs) :
  s.inf' hs f ^ n = s.inf' hs fun a ↦ f a ^ n

Full source

@[to_additive nsmul_inf']
lemma inf'_pow [LinearOrder M] [Monoid M] [MulLeftMono M] [MulRightMono M] (s : Finset ι)
    (f : ι → M) (n : ℕ) (hs) : s.inf' hs f ^ n = s.inf' hs fun a ↦ f a ^ n :=
  map_finset_inf' (OrderHom.mk _ <| pow_left_mono n) hs _

Power of Infimum Equals Infimum of Powers in Ordered Monoids

Informal description

Let $M$ be a linearly ordered monoid where multiplication is both left and right monotone. For any nonempty finite set $s$ indexed by $\iota$, any function $f \colon \iota \to M$, and any natural number $n$, the $n$-th power of the infimum of $f$ over $s$ is equal to the infimum of the $n$-th powers of $f$ over $s$. That is, \[ \left(\inf_{x \in s} f(x)\right)^n = \inf_{x \in s} (f(x))^n. \]

Finset.sup'_pow theorem

 [LinearOrder M] [Monoid M] [MulLeftMono M] [MulRightMono M] (s : Finset ι) (f : ι → M) (n : ℕ) (hs) :
  s.sup' hs f ^ n = s.sup' hs fun a ↦ f a ^ n

Full source

@[to_additive nsmul_sup']
lemma sup'_pow [LinearOrder M] [Monoid M] [MulLeftMono M] [MulRightMono M] (s : Finset ι)
    (f : ι → M) (n : ℕ) (hs) : s.sup' hs f ^ n = s.sup' hs fun a ↦ f a ^ n :=
  map_finset_sup' (OrderHom.mk _ <| pow_left_mono n) hs _

Power of Supremum Equals Supremum of Powers in Ordered Monoids

Informal description

Let $M$ be a linearly ordered monoid where multiplication is both left and right monotone. For any nonempty finite set $s$ indexed by $\iota$, any function $f : \iota \to M$, and any natural number $n$, the $n$-th power of the supremum of $f$ over $s$ is equal to the supremum of the $n$-th powers of $f$ over $s$. That is, \[ \left(\sup'_{x \in s} f(x)\right)^n = \sup'_{x \in s} (f(x))^n. \]

Finset.sup'_mul theorem

[MulRightMono G] (s : Finset ι) (f : ι → G) (a : G) (hs) : s.sup' hs f * a = s.sup' hs fun i ↦ f i * a

Full source

@[to_additive "Also see `Finset.sup'_add'` that works for canonically ordered monoids."]
lemma sup'_mul [MulRightMono G] (s : Finset ι) (f : ι → G) (a : G) (hs) :
    s.sup' hs f * a = s.sup' hs fun i ↦ f i * a := map_finset_sup' (OrderIso.mulRight a) hs f

Right Multiplication Commutes with Finite Supremum in Ordered Monoids: $(\sup f) * a = \sup (f * a)$

Informal description

Let $G$ be a linearly ordered monoid where right multiplication is monotone (i.e., for any $x, y, z \in G$, $x \leq y$ implies $x * z \leq y * z$). For any nonempty finite set $s$ indexed by $\iota$, any function $f : \iota \to G$, and any element $a \in G$, we have: \[ \left(\sup_{i \in s} f(i)\right) * a = \sup_{i \in s} (f(i) * a). \]

Finset.mul_sup' theorem

[MulLeftMono G] (s : Finset ι) (f : ι → G) (a : G) (hs) : a * s.sup' hs f = s.sup' hs fun i ↦ a * f i

Full source

@[to_additive "Also see `Finset.add_sup''` that works for canonically ordered monoids."]
lemma mul_sup' [MulLeftMono G] (s : Finset ι) (f : ι → G) (a : G) (hs) :
    a * s.sup' hs f = s.sup' hs fun i ↦ a * f i := map_finset_sup' (OrderIso.mulLeft a) hs f

Left Multiplication Commutes with Finite Supremum in Ordered Groups: $a \cdot \sup' s f = \sup' s (a \cdot f)$

Informal description

Let $G$ be a group with a linear order such that left multiplication by any element is order-preserving (i.e., $G$ is `MulLeftMono`). For any nonempty finite set $s$ indexed by $\iota$, any function $f \colon \iota \to G$, and any element $a \in G$, we have: \[ a \cdot \left(\sup'_{x \in s} f(x)\right) = \sup'_{x \in s} (a \cdot f(x)), \] where $\sup'$ denotes the supremum over the nonempty set $s$.

Finset.sup'_add' theorem

(s : Finset ι) (f : ι → M) (a : M) (hs : s.Nonempty) : s.sup' hs f + a = s.sup' hs fun i ↦ f i + a

Full source

/-- Also see `Finset.sup'_add` that works for ordered groups. -/
lemma sup'_add' (s : Finset ι) (f : ι → M) (a : M) (hs : s.Nonempty) :
    s.sup' hs f + a = s.sup' hs fun i ↦ f i + a := by
  apply le_antisymm
  · apply add_le_of_le_tsub_right_of_le
    · exact Finset.le_sup'_of_le _ hs.choose_spec le_add_self
    · exact Finset.sup'_le _ _ fun i hi ↦ le_tsub_of_add_le_right (Finset.le_sup' (f · + a) hi)
  · exact Finset.sup'_le _ _ fun i hi ↦ add_le_add_right (Finset.le_sup' _ hi) _

Right Addition Commutes with Finite Supremum in Ordered Additive Monoids: $(\sup f) + a = \sup (f + a)$

Informal description

Let $M$ be an additive commutative monoid with a linear order. For any nonempty finite set $s$ indexed by $\iota$, any function $f \colon \iota \to M$, and any element $a \in M$, we have: \[ \left(\sup_{i \in s} f(i)\right) + a = \sup_{i \in s} (f(i) + a). \]

Finset.add_sup'' theorem

(hs : s.Nonempty) (f : ι → M) (a : M) : a + s.sup' hs f = s.sup' hs fun i ↦ a + f i

Full source

/-- Also see `Finset.add_sup'` that works for ordered groups. -/
lemma add_sup'' (hs : s.Nonempty) (f : ι → M) (a : M) :
    a + s.sup' hs f = s.sup' hs fun i ↦ a + f i := by simp_rw [add_comm a, Finset.sup'_add']

Left Addition Commutes with Finite Supremum in Ordered Additive Monoids: $a + \sup' s f = \sup' s (a + f)$

Informal description

Let $M$ be an additive commutative monoid with a linear order. For any nonempty finite set $s$ indexed by $\iota$, any function $f \colon \iota \to M$, and any element $a \in M$, we have: \[ a + \left(\sup'_{i \in s} f(i)\right) = \sup'_{i \in s} (a + f(i)), \] where $\sup'$ denotes the supremum over the nonempty set $s$.

Finset.sup_add theorem

(hs : s.Nonempty) (f : ι → M) (a : M) : s.sup f + a = s.sup fun i ↦ f i + a

Full source

protected lemma sup_add (hs : s.Nonempty) (f : ι → M) (a : M) :
    s.sup f + a = s.sup fun i ↦ f i + a := by
  rw [← Finset.sup'_eq_sup hs, ← Finset.sup'_eq_sup hs, sup'_add']

Right Addition Commutes with Finite Supremum in Ordered Additive Monoids: $(\sup f) + a = \sup (f + a)$

Informal description

Let $M$ be an additive commutative monoid with a linear order. For any nonempty finite set $s$ indexed by $\iota$, any function $f \colon \iota \to M$, and any element $a \in M$, we have: \[ \left(\sup_{i \in s} f(i)\right) + a = \sup_{i \in s} (f(i) + a). \]

Finset.add_sup theorem

(hs : s.Nonempty) (f : ι → M) (a : M) : a + s.sup f = s.sup fun i ↦ a + f i

Full source

protected lemma add_sup (hs : s.Nonempty) (f : ι → M) (a : M) :
    a + s.sup f = s.sup fun i ↦ a + f i := by
  rw [← Finset.sup'_eq_sup hs, ← Finset.sup'_eq_sup hs, add_sup'']

Left Addition Commutes with Finite Supremum in Ordered Additive Monoids: $a + \sup s f = \sup s (a + f)$

Informal description

Let $M$ be an additive commutative monoid with a linear order. For any nonempty finite set $s$ indexed by $\iota$, any function $f \colon \iota \to M$, and any element $a \in M$, we have: \[ a + \left(\sup_{i \in s} f(i)\right) = \sup_{i \in s} (a + f(i)). \]

Finset.sup_add_sup theorem

 (hs : s.Nonempty) (ht : t.Nonempty) (f : ι → M) (g : κ → M) : s.sup f + t.sup g = (s ×ˢ t).sup fun ij ↦ f ij.1 + g ij.2

Full source

lemma sup_add_sup (hs : s.Nonempty) (ht : t.Nonempty) (f : ι → M) (g : κ → M) :
    s.sup f + t.sup g = (s ×ˢ t).sup fun ij ↦ f ij.1 + g ij.2 := by
  simp only [Finset.sup_add hs, Finset.add_sup ht, Finset.sup_product_left]

Supremum Addition Formula: $\sup f + \sup g = \sup (f + g)$ over Product Set

Informal description

Let $M$ be an additive commutative monoid with a linear order. For any nonempty finite sets $s \subseteq \iota$ and $t \subseteq \kappa$, and any functions $f \colon \iota \to M$ and $g \colon \kappa \to M$, we have: \[ \sup_{i \in s} f(i) + \sup_{j \in t} g(j) = \sup_{(i,j) \in s \times t} (f(i) + g(j)). \]