Lemmas about densely linearly ordered groups. #

theorem le_of_forall_lt_one_mul_le {α : Type u_1} [Group α] [LinearOrder α] [MulLeftMono α] [DenselyOrdered α] {a : α} {b : α} (h : ∀ (ε : α), ε < 1 → a * ε ≤ b) :

a ≤ b

theorem le_of_forall_neg_add_le {α : Type u_1} [AddGroup α] [LinearOrder α] [AddLeftMono α] [DenselyOrdered α] {a : α} {b : α} (h : ∀ (ε : α), ε < 0 → a + ε ≤ b) :

a ≤ b

theorem le_of_forall_one_lt_div_le {α : Type u_1} [Group α] [LinearOrder α] [MulLeftMono α] [DenselyOrdered α] {a : α} {b : α} (h : ∀ (ε : α), 1 < ε → a / ε ≤ b) :

a ≤ b

theorem le_of_forall_pos_sub_le {α : Type u_1} [AddGroup α] [LinearOrder α] [AddLeftMono α] [DenselyOrdered α] {a : α} {b : α} (h : ∀ (ε : α), 0 < ε → a - ε ≤ b) :

a ≤ b

a ≤ b ↔ ∀ (ε : α), 1 < ε → a ≤ b * ε

a ≤ b ↔ ∀ (ε : α), 0 < ε → a ≤ b + ε

a ≤ b ↔ ∀ (ε : α), ε < 1 → a * ε ≤ b

a ≤ b ↔ ∀ (ε : α), ε < 0 → a + ε ≤ b

theorem le_mul_of_forall_lt {α : Type u_1} [CommGroup α] [LinearOrder α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] [DenselyOrdered α] {a : α} {b : α} {c : α} (h : ∀ (a' : α), a' > a → ∀ (b' : α), b' > b → c ≤ a' * b') :

c ≤ a * b

theorem le_add_of_forall_lt {α : Type u_1} [AddCommGroup α] [LinearOrder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [DenselyOrdered α] {a : α} {b : α} {c : α} (h : ∀ (a' : α), a' > a → ∀ (b' : α), b' > b → c ≤ a' + b') :

c ≤ a + b

theorem mul_le_of_forall_lt {α : Type u_1} [CommGroup α] [LinearOrder α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] [DenselyOrdered α] {a : α} {b : α} {c : α} (h : ∀ (a' : α), a' < a → ∀ (b' : α), b' < b → a' * b' ≤ c) :

a * b ≤ c

theorem add_le_of_forall_lt {α : Type u_1} [AddCommGroup α] [LinearOrder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [DenselyOrdered α] {a : α} {b : α} {c : α} (h : ∀ (a' : α), a' < a → ∀ (b' : α), b' < b → a' + b' ≤ c) :

a + b ≤ c

Documentation