mathlib3 documentation

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.

source
theorem le_of_forall_lt_one_mul_le {α : Type u_1} [group α] [linear_order α] [covariant_class α α has_mul.mul has_le.le] [densely_ordered α] {a b : α} (h : ∀ (ε : α), ε < 1 → a * ε ≤ b) :
a ≤ b
source
theorem le_of_forall_neg_add_le {α : Type u_1} [add_group α] [linear_order α] [covariant_class α α has_add.add has_le.le] [densely_ordered α] {a b : α} (h : ∀ (ε : α), ε < 0 → a + ε ≤ b) :
a ≤ b
source
theorem le_of_forall_one_lt_div_le {α : Type u_1} [group α] [linear_order α] [covariant_class α α has_mul.mul has_le.le] [densely_ordered α] {a b : α} (h : ∀ (ε : α), 1 < ε → a / ε ≤ b) :
a ≤ b
source
theorem le_of_forall_pos_sub_le {α : Type u_1} [add_group α] [linear_order α] [covariant_class α α has_add.add has_le.le] [densely_ordered α] {a b : α} (h : ∀ (ε : α), 0 < ε → a - ε ≤ b) :
a ≤ b
source
theorem le_iff_forall_pos_le_add {α : Type u_1} [add_group α] [linear_order α] [covariant_class α α has_add.add has_le.le] [densely_ordered α] {a b : α} :
a ≤ b ↔ ∀ (ε : α), 0 < ε → a ≤ b + ε
source
theorem le_iff_forall_one_lt_le_mul {α : Type u_1} [group α] [linear_order α] [covariant_class α α has_mul.mul has_le.le] [densely_ordered α] {a b : α} :
a ≤ b ↔ ∀ (ε : α), 1 < ε → a ≤ b * ε
source
theorem le_iff_forall_neg_add_le {α : Type u_1} [add_group α] [linear_order α] [covariant_class α α has_add.add has_le.le] [densely_ordered α] {a b : α} :
a ≤ b ↔ ∀ (ε : α), ε < 0 → a + ε ≤ b
source
theorem le_iff_forall_lt_one_mul_le {α : Type u_1} [group α] [linear_order α] [covariant_class α α has_mul.mul has_le.le] [densely_ordered α] {a b : α} :
a ≤ b ↔ ∀ (ε : α), ε < 1 → a * ε ≤ b