Documentation

Mathlib.Algebra.Order.Group.CompleteLattice

Distributivity of group operations over supremum/infimum #

theorem ciSup_add {ι : Type u_1} {G : Type u_2} [AddGroup G] [ConditionallyCompleteLattice G] [Nonempty ι] {f : ιG} [AddRightMono G] (hf : BddAbove (Set.range f)) (a : G) :
(⨆ (i : ι), f i) + a = ⨆ (i : ι), f i + a
theorem ciSup_mul {ι : Type u_1} {G : Type u_2} [Group G] [ConditionallyCompleteLattice G] [Nonempty ι] {f : ιG} [MulRightMono G] (hf : BddAbove (Set.range f)) (a : G) :
(⨆ (i : ι), f i) * a = ⨆ (i : ι), f i * a
theorem ciSup_sub {ι : Type u_1} {G : Type u_2} [AddGroup G] [ConditionallyCompleteLattice G] [Nonempty ι] {f : ιG} [AddRightMono G] (hf : BddAbove (Set.range f)) (a : G) :
(⨆ (i : ι), f i) - a = ⨆ (i : ι), f i - a
theorem ciSup_div {ι : Type u_1} {G : Type u_2} [Group G] [ConditionallyCompleteLattice G] [Nonempty ι] {f : ιG} [MulRightMono G] (hf : BddAbove (Set.range f)) (a : G) :
(⨆ (i : ι), f i) / a = ⨆ (i : ι), f i / a
theorem ciInf_add {ι : Type u_1} {G : Type u_2} [AddGroup G] [ConditionallyCompleteLattice G] [Nonempty ι] {f : ιG} [AddRightMono G] (hf : BddBelow (Set.range f)) (a : G) :
(⨅ (i : ι), f i) + a = ⨅ (i : ι), f i + a
theorem ciInf_mul {ι : Type u_1} {G : Type u_2} [Group G] [ConditionallyCompleteLattice G] [Nonempty ι] {f : ιG} [MulRightMono G] (hf : BddBelow (Set.range f)) (a : G) :
(⨅ (i : ι), f i) * a = ⨅ (i : ι), f i * a
theorem ciInf_sub {ι : Type u_1} {G : Type u_2} [AddGroup G] [ConditionallyCompleteLattice G] [Nonempty ι] {f : ιG} [AddRightMono G] (hf : BddBelow (Set.range f)) (a : G) :
(⨅ (i : ι), f i) - a = ⨅ (i : ι), f i - a
theorem ciInf_div {ι : Type u_1} {G : Type u_2} [Group G] [ConditionallyCompleteLattice G] [Nonempty ι] {f : ιG} [MulRightMono G] (hf : BddBelow (Set.range f)) (a : G) :
(⨅ (i : ι), f i) / a = ⨅ (i : ι), f i / a
theorem add_ciSup {ι : Type u_1} {G : Type u_2} [AddGroup G] [ConditionallyCompleteLattice G] [Nonempty ι] {f : ιG} [AddLeftMono G] (hf : BddAbove (Set.range f)) (a : G) :
a + ⨆ (i : ι), f i = ⨆ (i : ι), a + f i
theorem mul_ciSup {ι : Type u_1} {G : Type u_2} [Group G] [ConditionallyCompleteLattice G] [Nonempty ι] {f : ιG} [MulLeftMono G] (hf : BddAbove (Set.range f)) (a : G) :
a * ⨆ (i : ι), f i = ⨆ (i : ι), a * f i
theorem add_ciInf {ι : Type u_1} {G : Type u_2} [AddGroup G] [ConditionallyCompleteLattice G] [Nonempty ι] {f : ιG} [AddLeftMono G] (hf : BddBelow (Set.range f)) (a : G) :
a + ⨅ (i : ι), f i = ⨅ (i : ι), a + f i
theorem mul_ciInf {ι : Type u_1} {G : Type u_2} [Group G] [ConditionallyCompleteLattice G] [Nonempty ι] {f : ιG} [MulLeftMono G] (hf : BddBelow (Set.range f)) (a : G) :
a * ⨅ (i : ι), f i = ⨅ (i : ι), a * f i