Conditionally complete lattices and groups. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
theorem
le_add_cinfi
{α : Type u_1}
{ι : Sort u_2}
[nonempty ι]
[conditionally_complete_lattice α]
[add_group α]
[covariant_class α α has_add.add has_le.le]
{a g : α}
{h : ι → α}
(H : ∀ (j : ι), a ≤ g + h j) :
theorem
le_mul_cinfi
{α : Type u_1}
{ι : Sort u_2}
[nonempty ι]
[conditionally_complete_lattice α]
[group α]
[covariant_class α α has_mul.mul has_le.le]
{a g : α}
{h : ι → α}
(H : ∀ (j : ι), a ≤ g * h j) :
theorem
mul_csupr_le
{α : Type u_1}
{ι : Sort u_2}
[nonempty ι]
[conditionally_complete_lattice α]
[group α]
[covariant_class α α has_mul.mul has_le.le]
{a g : α}
{h : ι → α}
(H : ∀ (j : ι), g * h j ≤ a) :
theorem
add_csupr_le
{α : Type u_1}
{ι : Sort u_2}
[nonempty ι]
[conditionally_complete_lattice α]
[add_group α]
[covariant_class α α has_add.add has_le.le]
{a g : α}
{h : ι → α}
(H : ∀ (j : ι), g + h j ≤ a) :
theorem
le_cinfi_add
{α : Type u_1}
{ι : Sort u_2}
[nonempty ι]
[conditionally_complete_lattice α]
[add_group α]
[covariant_class α α (function.swap has_add.add) has_le.le]
{a : α}
{g : ι → α}
{h : α}
(H : ∀ (i : ι), a ≤ g i + h) :
theorem
le_cinfi_mul
{α : Type u_1}
{ι : Sort u_2}
[nonempty ι]
[conditionally_complete_lattice α]
[group α]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
{a : α}
{g : ι → α}
{h : α}
(H : ∀ (i : ι), a ≤ g i * h) :
theorem
csupr_mul_le
{α : Type u_1}
{ι : Sort u_2}
[nonempty ι]
[conditionally_complete_lattice α]
[group α]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
{a : α}
{g : ι → α}
{h : α}
(H : ∀ (i : ι), g i * h ≤ a) :
theorem
csupr_add_le
{α : Type u_1}
{ι : Sort u_2}
[nonempty ι]
[conditionally_complete_lattice α]
[add_group α]
[covariant_class α α (function.swap has_add.add) has_le.le]
{a : α}
{g : ι → α}
{h : α}
(H : ∀ (i : ι), g i + h ≤ a) :
theorem
le_cinfi_mul_cinfi
{α : Type u_1}
{ι : Sort u_2}
{ι' : Sort u_3}
[nonempty ι]
[nonempty ι']
[conditionally_complete_lattice α]
[group α]
[covariant_class α α has_mul.mul has_le.le]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
{a : α}
{g : ι → α}
{h : ι' → α}
(H : ∀ (i : ι) (j : ι'), a ≤ g i * h j) :
theorem
le_cinfi_add_cinfi
{α : Type u_1}
{ι : Sort u_2}
{ι' : Sort u_3}
[nonempty ι]
[nonempty ι']
[conditionally_complete_lattice α]
[add_group α]
[covariant_class α α has_add.add has_le.le]
[covariant_class α α (function.swap has_add.add) has_le.le]
{a : α}
{g : ι → α}
{h : ι' → α}
(H : ∀ (i : ι) (j : ι'), a ≤ g i + h j) :
theorem
csupr_mul_csupr_le
{α : Type u_1}
{ι : Sort u_2}
{ι' : Sort u_3}
[nonempty ι]
[nonempty ι']
[conditionally_complete_lattice α]
[group α]
[covariant_class α α has_mul.mul has_le.le]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
{a : α}
{g : ι → α}
{h : ι' → α}
(H : ∀ (i : ι) (j : ι'), g i * h j ≤ a) :
theorem
csupr_add_csupr_le
{α : Type u_1}
{ι : Sort u_2}
{ι' : Sort u_3}
[nonempty ι]
[nonempty ι']
[conditionally_complete_lattice α]
[add_group α]
[covariant_class α α has_add.add has_le.le]
[covariant_class α α (function.swap has_add.add) has_le.le]
{a : α}
{g : ι → α}
{h : ι' → α}
(H : ∀ (i : ι) (j : ι'), g i + h j ≤ a) :