Conditionally complete lattices and groups.

theorem le_add_ciInf {α : Type u_1} {ι : Sort u_2} [Nonempty ι] [ConditionallyCompleteLattice α] [AddGroup α] [CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {g : α} {h : ι → α} (H : ∀ (j : ι), a ≤ g + h j) : a ≤ g + iInf h

theorem le_mul_ciInf {α : Type u_1} {ι : Sort u_2} [Nonempty ι] [ConditionallyCompleteLattice α] [Group α] [CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {g : α} {h : ι → α} (H : ∀ (j : ι), a ≤ g * h j) : a ≤ g * iInf h

theorem add_ciSup_le {α : Type u_1} {ι : Sort u_2} [Nonempty ι] [ConditionallyCompleteLattice α] [AddGroup α] [CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {g : α} {h : ι → α} (H : ∀ (j : ι), g + h j ≤ a) : g + iSup h ≤ a

theorem mul_ciSup_le {α : Type u_1} {ι : Sort u_2} [Nonempty ι] [ConditionallyCompleteLattice α] [Group α] [CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {g : α} {h : ι → α} (H : ∀ (j : ι), g * h j ≤ a) : g * iSup h ≤ a

theorem le_ciInf_add {α : Type u_1} {ι : Sort u_2} [Nonempty ι] [ConditionallyCompleteLattice α] [AddGroup α] [CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {g : ι → α} {h : α} (H : ∀ (i : ι), a ≤ g i + h) : a ≤ iInf g + h

theorem le_ciInf_mul {α : Type u_1} {ι : Sort u_2} [Nonempty ι] [ConditionallyCompleteLattice α] [Group α] [CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {g : ι → α} {h : α} (H : ∀ (i : ι), a ≤ g i * h) : a ≤ iInf g * h

theorem ciSup_add_le {α : Type u_1} {ι : Sort u_2} [Nonempty ι] [ConditionallyCompleteLattice α] [AddGroup α] [CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {g : ι → α} {h : α} (H : ∀ (i : ι), g i + h ≤ a) : iSup g + h ≤ a

theorem ciSup_mul_le {α : Type u_1} {ι : Sort u_2} [Nonempty ι] [ConditionallyCompleteLattice α] [Group α] [CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {g : ι → α} {h : α} (H : ∀ (i : ι), g i * h ≤ a) : iSup g * h ≤ a

theorem le_ciInf_add_ciInf {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} [Nonempty ι] [Nonempty ι'] [ConditionallyCompleteLattice α] [AddGroup α] [CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {g : ι → α} {h : ι' → α} (H : ∀ (i : ι) (j : ι'), a ≤ g i + h j) : a ≤ iInf g + iInf h

theorem le_ciInf_mul_ciInf {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} [Nonempty ι] [Nonempty ι'] [ConditionallyCompleteLattice α] [Group α] [CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {g : ι → α} {h : ι' → α} (H : ∀ (i : ι) (j : ι'), a ≤ g i * h j) : a ≤ iInf g * iInf h

theorem ciSup_add_ciSup_le {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} [Nonempty ι] [Nonempty ι'] [ConditionallyCompleteLattice α] [AddGroup α] [CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {g : ι → α} {h : ι' → α} (H : ∀ (i : ι) (j : ι'), g i + h j ≤ a) : iSup g + iSup h ≤ a

theorem ciSup_mul_ciSup_le {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} [Nonempty ι] [Nonempty ι'] [ConditionallyCompleteLattice α] [Group α] [CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {g : ι → α} {h : ι' → α} (H : ∀ (i : ι) (j : ι'), g i * h j ≤ a) : iSup g * iSup h ≤ a