Documentation

Mathlib.Order.ConditionallyCompleteLattice.Group

Conditionally complete lattices and groups. #

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
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
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
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
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
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
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
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
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) :
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) :
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) :
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) :