Documentation

Mathlib.Algebra.Order.Group.Finset

Finset.sup in a group #

source
theorem Finset.fold_max_add {ι : Type u_1} {M : Type u_3} [LinearOrder M] [Add M] [AddRightMono M] (s : Finset ι) (a : WithBot M) (f : ι → M) :
Finset.fold max ⊥ (fun (i : ι) => ↑(f i) + a) s = Finset.fold max ⊥ (WithBot.some ∘ f) s + a
source
theorem Finset.inf'_pow {ι : Type u_1} {M : Type u_3} [LinearOrder M] [Monoid M] [MulLeftMono M] [MulRightMono M] (s : Finset ι) (f : ι → M) (n : ℕ) (hs : s.Nonempty) :
s.inf' hs f ^ n = s.inf' hs fun (a : ι) => f a ^ n
source
theorem Finset.nsmul_inf' {ι : Type u_1} {M : Type u_3} [LinearOrder M] [AddMonoid M] [AddLeftMono M] [AddRightMono M] (s : Finset ι) (f : ι → M) (n : ℕ) (hs : s.Nonempty) :
n • s.inf' hs f = s.inf' hs fun (a : ι) => n • f a
source
theorem Finset.sup'_pow {ι : Type u_1} {M : Type u_3} [LinearOrder M] [Monoid M] [MulLeftMono M] [MulRightMono M] (s : Finset ι) (f : ι → M) (n : ℕ) (hs : s.Nonempty) :
s.sup' hs f ^ n = s.sup' hs fun (a : ι) => f a ^ n
source
theorem Finset.nsmul_sup' {ι : Type u_1} {M : Type u_3} [LinearOrder M] [AddMonoid M] [AddLeftMono M] [AddRightMono M] (s : Finset ι) (f : ι → M) (n : ℕ) (hs : s.Nonempty) :
n • s.sup' hs f = s.sup' hs fun (a : ι) => n • f a
source
theorem Finset.sup'_mul {ι : Type u_1} {G : Type u_4} [Group G] [LinearOrder G] [MulRightMono G] (s : Finset ι) (f : ι → G) (a : G) (hs : s.Nonempty) :
s.sup' hs f * a = s.sup' hs fun (i : ι) => f i * a
source
theorem Finset.sup'_add {ι : Type u_1} {G : Type u_4} [AddGroup G] [LinearOrder G] [AddRightMono G] (s : Finset ι) (f : ι → G) (a : G) (hs : s.Nonempty) :
s.sup' hs f + a = s.sup' hs fun (i : ι) => f i + a

Also see Finset.sup'_add' that works for canonically ordered monoids.

source
theorem Finset.mul_sup' {ι : Type u_1} {G : Type u_4} [Group G] [LinearOrder G] [MulLeftMono G] (s : Finset ι) (f : ι → G) (a : G) (hs : s.Nonempty) :
a * s.sup' hs f = s.sup' hs fun (i : ι) => a * f i
source
theorem Finset.add_sup' {ι : Type u_1} {G : Type u_4} [AddGroup G] [LinearOrder G] [AddLeftMono G] (s : Finset ι) (f : ι → G) (a : G) (hs : s.Nonempty) :
a + s.sup' hs f = s.sup' hs fun (i : ι) => a + f i

Also see Finset.add_sup'' that works for canonically ordered monoids.

source
theorem Finset.sup'_add' {ι : Type u_1} {M : Type u_3} [CanonicallyLinearOrderedAddCommMonoid M] [Sub M] [AddLeftReflectLE M] [OrderedSub M] (s : Finset ι) (f : ι → M) (a : M) (hs : s.Nonempty) :
s.sup' hs f + a = s.sup' hs fun (i : ι) => f i + a

Also see Finset.sup'_add that works for ordered groups.

source
theorem Finset.add_sup'' {ι : Type u_1} {M : Type u_3} [CanonicallyLinearOrderedAddCommMonoid M] [Sub M] [AddLeftReflectLE M] [OrderedSub M] {s : Finset ι} (hs : s.Nonempty) (f : ι → M) (a : M) :
a + s.sup' hs f = s.sup' hs fun (i : ι) => a + f i

Also see Finset.add_sup' that works for ordered groups.

source
theorem Finset.sup_add {ι : Type u_1} {M : Type u_3} [CanonicallyLinearOrderedAddCommMonoid M] [Sub M] [AddLeftReflectLE M] [OrderedSub M] {s : Finset ι} (hs : s.Nonempty) (f : ι → M) (a : M) :
s.sup f + a = s.sup fun (i : ι) => f i + a
source
theorem Finset.add_sup {ι : Type u_1} {M : Type u_3} [CanonicallyLinearOrderedAddCommMonoid M] [Sub M] [AddLeftReflectLE M] [OrderedSub M] {s : Finset ι} (hs : s.Nonempty) (f : ι → M) (a : M) :
a + s.sup f = s.sup fun (i : ι) => a + f i
source
theorem Finset.sup_add_sup {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [CanonicallyLinearOrderedAddCommMonoid M] [Sub M] [AddLeftReflectLE M] [OrderedSub M] {s : Finset ι} {t : Finset κ} (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