Complete lattices and groups

theorem iSup_mul_le {α : Type u_1} {ι : Sort u_2} [CompleteLattice α] [Mul α] [MulLeftMono α] [MulRightMono α] (u v : ι → α) : ⨆ (i : ι), u i * v i ≤ (⨆ (i : ι), u i) * ⨆ (i : ι), v i

theorem iSup_add_le {α : Type u_1} {ι : Sort u_2} [CompleteLattice α] [Add α] [AddLeftMono α] [AddRightMono α] (u v : ι → α) : ⨆ (i : ι), u i + v i ≤ (⨆ (i : ι), u i) + ⨆ (i : ι), v i

theorem le_iInf_mul {α : Type u_1} {ι : Sort u_2} [CompleteLattice α] [Mul α] [MulLeftMono α] [MulRightMono α] (u v : ι → α) : (⨅ (i : ι), u i) * ⨅ (i : ι), v i ≤ ⨅ (i : ι), u i * v i

theorem le_iInf_add {α : Type u_1} {ι : Sort u_2} [CompleteLattice α] [Add α] [AddLeftMono α] [AddRightMono α] (u v : ι → α) : (⨅ (i : ι), u i) + ⨅ (i : ι), v i ≤ ⨅ (i : ι), u i + v i

theorem iSup₂_mul_le {α : Type u_1} {ι : Sort u_2} {κ : ι → Sort u_3} [CompleteLattice α] [Mul α] [MulLeftMono α] [MulRightMono α] (u v : (i : ι) → κ i → α) : ⨆ (i : ι), ⨆ (j : κ i), u i j * v i j ≤ (⨆ (i : ι), ⨆ (j : κ i), u i j) * ⨆ (i : ι), ⨆ (j : κ i), v i j

theorem iSup₂_add_le {α : Type u_1} {ι : Sort u_2} {κ : ι → Sort u_3} [CompleteLattice α] [Add α] [AddLeftMono α] [AddRightMono α] (u v : (i : ι) → κ i → α) : ⨆ (i : ι), ⨆ (j : κ i), u i j + v i j ≤ (⨆ (i : ι), ⨆ (j : κ i), u i j) + ⨆ (i : ι), ⨆ (j : κ i), v i j

theorem le_iInf₂_mul {α : Type u_1} {ι : Sort u_2} {κ : ι → Sort u_3} [CompleteLattice α] [Mul α] [MulLeftMono α] [MulRightMono α] (u v : (i : ι) → κ i → α) : (⨅ (i : ι), ⨅ (j : κ i), u i j) * ⨅ (i : ι), ⨅ (j : κ i), v i j ≤ ⨅ (i : ι), ⨅ (j : κ i), u i j * v i j

theorem le_iInf₂_add {α : Type u_1} {ι : Sort u_2} {κ : ι → Sort u_3} [CompleteLattice α] [Add α] [AddLeftMono α] [AddRightMono α] (u v : (i : ι) → κ i → α) : (⨅ (i : ι), ⨅ (j : κ i), u i j) + ⨅ (i : ι), ⨅ (j : κ i), v i j ≤ ⨅ (i : ι), ⨅ (j : κ i), u i j + v i j