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} [CovariantClass G G (Function.swap fun (x1 x2 : G) => x1 + x2) fun (x1 x2 : G) => x1 x2] (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} [CovariantClass G G (Function.swap fun (x1 x2 : G) => x1 * x2) fun (x1 x2 : G) => x1 x2] (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} [CovariantClass G G (Function.swap fun (x1 x2 : G) => x1 + x2) fun (x1 x2 : G) => x1 x2] (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} [CovariantClass G G (Function.swap fun (x1 x2 : G) => x1 * x2) fun (x1 x2 : G) => x1 x2] (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} [CovariantClass G G (Function.swap fun (x1 x2 : G) => x1 + x2) fun (x1 x2 : G) => x1 x2] (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} [CovariantClass G G (Function.swap fun (x1 x2 : G) => x1 * x2) fun (x1 x2 : G) => x1 x2] (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} [CovariantClass G G (Function.swap fun (x1 x2 : G) => x1 + x2) fun (x1 x2 : G) => x1 x2] (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} [CovariantClass G G (Function.swap fun (x1 x2 : G) => x1 * x2) fun (x1 x2 : G) => x1 x2] (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} [CovariantClass G G (fun (x1 x2 : G) => x1 + x2) fun (x1 x2 : G) => x1 x2] (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} [CovariantClass G G (fun (x1 x2 : G) => x1 * x2) fun (x1 x2 : G) => x1 x2] (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} [CovariantClass G G (fun (x1 x2 : G) => x1 + x2) fun (x1 x2 : G) => x1 x2] (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} [CovariantClass G G (fun (x1 x2 : G) => x1 * x2) fun (x1 x2 : G) => x1 x2] (hf : BddBelow (Set.range f)) (a : G) :
a * ⨅ (i : ι), f i = ⨅ (i : ι), a * f i