Documentation

Mathlib.Algebra.Order.Group.DenselyOrdered

Lemmas about densely linearly ordered groups. #

theorem le_of_forall_neg_add_le {α : Type u_1} [AddGroup α] [LinearOrder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [DenselyOrdered α] {a : α} {b : α} (h : ∀ (ε : α), ε < 0a + ε b) :
a b
theorem le_of_forall_lt_one_mul_le {α : Type u_1} [Group α] [LinearOrder α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] [DenselyOrdered α] {a : α} {b : α} (h : ∀ (ε : α), ε < 1a * ε b) :
a b
theorem le_of_forall_pos_sub_le {α : Type u_1} [AddGroup α] [LinearOrder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [DenselyOrdered α] {a : α} {b : α} (h : ∀ (ε : α), 0 < εa - ε b) :
a b
theorem le_of_forall_one_lt_div_le {α : Type u_1} [Group α] [LinearOrder α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] [DenselyOrdered α] {a : α} {b : α} (h : ∀ (ε : α), 1 < εa / ε b) :
a b
theorem le_iff_forall_pos_le_add {α : Type u_1} [AddGroup α] [LinearOrder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [DenselyOrdered α] {a : α} {b : α} :
a b ∀ (ε : α), 0 < εa b + ε
theorem le_iff_forall_one_lt_le_mul {α : Type u_1} [Group α] [LinearOrder α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] [DenselyOrdered α] {a : α} {b : α} :
a b ∀ (ε : α), 1 < εa b * ε
theorem le_iff_forall_neg_add_le {α : Type u_1} [AddGroup α] [LinearOrder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [DenselyOrdered α] {a : α} {b : α} :
a b ∀ (ε : α), ε < 0a + ε b
theorem le_iff_forall_lt_one_mul_le {α : Type u_1} [Group α] [LinearOrder α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] [DenselyOrdered α] {a : α} {b : α} :
a b ∀ (ε : α), ε < 1a * ε b