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 : ∀ (ε : α), ε < 0 → a + ε ≤ 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 : ∀ (ε : α), ε < 1 → a * ε ≤ 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 : α}
:
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 : α}
:
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 : α}
:
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 : α}
: