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