Conditionally complete lattices and groups.

ink

theorem le_add_cinfᵢ {α : Type u_1} {ι : Sort u_2} [inst : Nonempty ι] [inst : ConditionallyCompleteLattice α] [inst : AddGroup α] [inst : 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 + infᵢ h

ink

theorem le_mul_cinfᵢ {α : Type u_1} {ι : Sort u_2} [inst : Nonempty ι] [inst : ConditionallyCompleteLattice α] [inst : Group α] [inst : 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 * infᵢ h

ink

theorem add_csupᵢ_le {α : Type u_1} {ι : Sort u_2} [inst : Nonempty ι] [inst : ConditionallyCompleteLattice α] [inst : AddGroup α] [inst : 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 + supᵢ h ≤ a

ink

theorem mul_csupᵢ_le {α : Type u_1} {ι : Sort u_2} [inst : Nonempty ι] [inst : ConditionallyCompleteLattice α] [inst : Group α] [inst : 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 * supᵢ h ≤ a

ink

theorem le_cinfᵢ_add {α : Type u_1} {ι : Sort u_2} [inst : Nonempty ι] [inst : ConditionallyCompleteLattice α] [inst : AddGroup α] [inst : 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 ≤ infᵢ g + h

ink

theorem le_cinfᵢ_mul {α : Type u_1} {ι : Sort u_2} [inst : Nonempty ι] [inst : ConditionallyCompleteLattice α] [inst : Group α] [inst : 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 ≤ infᵢ g * h

ink

theorem csupᵢ_add_le {α : Type u_1} {ι : Sort u_2} [inst : Nonempty ι] [inst : ConditionallyCompleteLattice α] [inst : AddGroup α] [inst : 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) : supᵢ g + h ≤ a

ink

theorem csupᵢ_mul_le {α : Type u_1} {ι : Sort u_2} [inst : Nonempty ι] [inst : ConditionallyCompleteLattice α] [inst : Group α] [inst : 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) : supᵢ g * h ≤ a

ink

theorem le_cinfᵢ_add_cinfᵢ {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} [inst : Nonempty ι] [inst : Nonempty ι'] [inst : ConditionallyCompleteLattice α] [inst : AddGroup α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst : 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 ≤ infᵢ g + infᵢ h

ink

theorem le_cinfᵢ_mul_cinfᵢ {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} [inst : Nonempty ι] [inst : Nonempty ι'] [inst : ConditionallyCompleteLattice α] [inst : Group α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst : 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 ≤ infᵢ g * infᵢ h

ink

theorem csupᵢ_add_csupᵢ_le {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} [inst : Nonempty ι] [inst : Nonempty ι'] [inst : ConditionallyCompleteLattice α] [inst : AddGroup α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst : 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) : supᵢ g + supᵢ h ≤ a

ink

theorem csupᵢ_mul_csupᵢ_le {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} [inst : Nonempty ι] [inst : Nonempty ι'] [inst : ConditionallyCompleteLattice α] [inst : Group α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst : 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) : supᵢ g * supᵢ h ≤ a