Conditionally complete lattices and groups. #
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)
:
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)
:
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)
:
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)
:
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)
: