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