mathlib3 documentation

order.conditionally_complete_lattice.group

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) :
a g + infi h
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) :
a g * infi h
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) :
g * supr h 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) :
g + supr h 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) :
a infi g + 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) :
a infi g * 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) :
supr g * 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) :
supr g + 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) :
a infi g * infi h
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) :
a infi g + infi h
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) :
supr g * supr h 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) :
supr g + supr h a