Documentation

Mathlib.Order.ConditionallyCompleteLattice.Group

Conditionally complete lattices and groups. #

source
theorem ciSup_mul_le_ciSup_mul_ciSup {α : Type u_1} {ι : Sort u_2} [Nonempty ι] [ConditionallyCompleteLattice α] [Mul α] [MulLeftMono α] [MulRightMono α] {f g : ι → α} (hf : BddAbove (Set.range f)) (hg : BddAbove (Set.range g)) :
⨆ (i : ι), f i * g i ≤ (⨆ (i : ι), f i) * ⨆ (i : ι), g i
source
theorem ciSup_add_le_ciSup_add_ciSup {α : Type u_1} {ι : Sort u_2} [Nonempty ι] [ConditionallyCompleteLattice α] [Add α] [AddLeftMono α] [AddRightMono α] {f g : ι → α} (hf : BddAbove (Set.range f)) (hg : BddAbove (Set.range g)) :
⨆ (i : ι), f i + g i ≤ (⨆ (i : ι), f i) + ⨆ (i : ι), g i
source
theorem ciInf_mul_ciInf_le_ciInf_mul {α : Type u_1} {ι : Sort u_2} [Nonempty ι] [ConditionallyCompleteLattice α] [Mul α] [MulLeftMono α] [MulRightMono α] {f g : ι → α} (hf : BddBelow (Set.range f)) (hg : BddBelow (Set.range g)) :
(⨅ (i : ι), f i) * ⨅ (i : ι), g i ≤ ⨅ (i : ι), f i * g i
source
theorem ciInf_add_ciInf_le_ciInf_add {α : Type u_1} {ι : Sort u_2} [Nonempty ι] [ConditionallyCompleteLattice α] [Add α] [AddLeftMono α] [AddRightMono α] {f g : ι → α} (hf : BddBelow (Set.range f)) (hg : BddBelow (Set.range g)) :
(⨅ (i : ι), f i) + ⨅ (i : ι), g i ≤ ⨅ (i : ι), f i + g i
source
theorem le_mul_ciInf {α : Type u_1} {ι : Sort u_2} [Nonempty ι] [ConditionallyCompleteLattice α] [Group α] [MulLeftMono α] {a g : α} {h : ι → α} (H : ∀ (j : ι), a ≤ g * h j) :
a ≤ g * iInf h
source
theorem le_add_ciInf {α : Type u_1} {ι : Sort u_2} [Nonempty ι] [ConditionallyCompleteLattice α] [AddGroup α] [AddLeftMono α] {a g : α} {h : ι → α} (H : ∀ (j : ι), a ≤ g + h j) :
a ≤ g + iInf h
source
theorem mul_ciSup_le {α : Type u_1} {ι : Sort u_2} [Nonempty ι] [ConditionallyCompleteLattice α] [Group α] [MulLeftMono α] {a g : α} {h : ι → α} (H : ∀ (j : ι), g * h j ≤ a) :
g * iSup h ≤ a
source
theorem add_ciSup_le {α : Type u_1} {ι : Sort u_2} [Nonempty ι] [ConditionallyCompleteLattice α] [AddGroup α] [AddLeftMono α] {a g : α} {h : ι → α} (H : ∀ (j : ι), g + h j ≤ a) :
g + iSup h ≤ a
source
theorem le_ciInf_mul {α : Type u_1} {ι : Sort u_2} [Nonempty ι] [ConditionallyCompleteLattice α] [Group α] [MulRightMono α] {a : α} {g : ι → α} {h : α} (H : ∀ (i : ι), a ≤ g i * h) :
a ≤ iInf g * h
source
theorem le_ciInf_add {α : Type u_1} {ι : Sort u_2} [Nonempty ι] [ConditionallyCompleteLattice α] [AddGroup α] [AddRightMono α] {a : α} {g : ι → α} {h : α} (H : ∀ (i : ι), a ≤ g i + h) :
a ≤ iInf g + h
source
theorem ciSup_mul_le {α : Type u_1} {ι : Sort u_2} [Nonempty ι] [ConditionallyCompleteLattice α] [Group α] [MulRightMono α] {a : α} {g : ι → α} {h : α} (H : ∀ (i : ι), g i * h ≤ a) :
iSup g * h ≤ a
source
theorem ciSup_add_le {α : Type u_1} {ι : Sort u_2} [Nonempty ι] [ConditionallyCompleteLattice α] [AddGroup α] [AddRightMono α] {a : α} {g : ι → α} {h : α} (H : ∀ (i : ι), g i + h ≤ a) :
iSup g + h ≤ a
source
theorem le_ciInf_mul_ciInf {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} [Nonempty ι] [Nonempty ι'] [ConditionallyCompleteLattice α] [Group α] [MulLeftMono α] [MulRightMono α] {a : α} {g : ι → α} {h : ι' → α} (H : ∀ (i : ι) (j : ι'), a ≤ g i * h j) :
a ≤ iInf g * iInf h
source
theorem le_ciInf_add_ciInf {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} [Nonempty ι] [Nonempty ι'] [ConditionallyCompleteLattice α] [AddGroup α] [AddLeftMono α] [AddRightMono α] {a : α} {g : ι → α} {h : ι' → α} (H : ∀ (i : ι) (j : ι'), a ≤ g i + h j) :
a ≤ iInf g + iInf h
source
theorem ciSup_mul_ciSup_le {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} [Nonempty ι] [Nonempty ι'] [ConditionallyCompleteLattice α] [Group α] [MulLeftMono α] [MulRightMono α] {a : α} {g : ι → α} {h : ι' → α} (H : ∀ (i : ι) (j : ι'), g i * h j ≤ a) :
iSup g * iSup h ≤ a
source
theorem ciSup_add_ciSup_le {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} [Nonempty ι] [Nonempty ι'] [ConditionallyCompleteLattice α] [AddGroup α] [AddLeftMono α] [AddRightMono α] {a : α} {g : ι → α} {h : ι' → α} (H : ∀ (i : ι) (j : ι'), g i + h j ≤ a) :
iSup g + iSup h ≤ a