Documentation

Mathlib.Order.ConditionallyCompleteLattice.Group

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