# mathlib3documentation

algebra.order.group.densely_ordered

# Lemmas about densely linearly ordered groups. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

theorem le_of_forall_lt_one_mul_le {α : Type u_1} [group α] [linear_order α] {a b : α} (h : (ε : α), ε < 1 a * ε b) :
a b
theorem le_of_forall_neg_add_le {α : Type u_1} [add_group α] [linear_order α] {a b : α} (h : (ε : α), ε < 0 a + ε b) :
a b
theorem le_of_forall_one_lt_div_le {α : Type u_1} [group α] [linear_order α] {a b : α} (h : (ε : α), 1 < ε a / ε b) :
a b
theorem le_of_forall_pos_sub_le {α : Type u_1} [add_group α] [linear_order α] {a b : α} (h : (ε : α), 0 < ε a - ε b) :
a b
theorem le_iff_forall_pos_le_add {α : Type u_1} [add_group α] [linear_order α] {a b : α} :
a b (ε : α), 0 < ε a b + ε
theorem le_iff_forall_one_lt_le_mul {α : Type u_1} [group α] [linear_order α] {a b : α} :
a b (ε : α), 1 < ε a b * ε
theorem le_iff_forall_neg_add_le {α : Type u_1} [add_group α] [linear_order α] {a b : α} :
a b (ε : α), ε < 0 a + ε b
theorem le_iff_forall_lt_one_mul_le {α : Type u_1} [group α] [linear_order α] {a b : α} :
a b (ε : α), ε < 1 a * ε b