Unbundled and weaker forms of canonically ordered monoids

class ExistsMulOfLE (α : Type u) [Mul α] [LE α] : Prop

An OrderedCommMonoid with one-sided 'division' in the sense that if a ≤ b, there is some c for which a * c = b. This is a weaker version of the condition on canonical orderings defined by CanonicallyOrderedCommMonoid.

• exists_mul_of_le : ∀ {a b : α}, a ≤ b → ∃ (c : α), b = a * c

  For a ≤ b, a left divides b

theorem ExistsMulOfLE.exists_mul_of_le {α : Type u} [Mul α] [LE α] [self : ExistsMulOfLE α] {a : α} {b : α} : a ≤ b → ∃ (c : α), b = a * c

For a ≤ b, a left divides b

class ExistsAddOfLE (α : Type u) [Add α] [LE α] : Prop

An OrderedAddCommMonoid with one-sided 'subtraction' in the sense that if a ≤ b, then there is some c for which a + c = b. This is a weaker version of the condition on canonical orderings defined by CanonicallyOrderedAddCommMonoid.

• exists_add_of_le : ∀ {a b : α}, a ≤ b → ∃ (c : α), b = a + c

  For a ≤ b, there is a c so b = a + c.

theorem ExistsAddOfLE.exists_add_of_le {α : Type u} [Add α] [LE α] [self : ExistsAddOfLE α] {a : α} {b : α} : a ≤ b → ∃ (c : α), b = a + c

For a ≤ b, there is a c so b = a + c.

@[instance 100]

instance AddGroup.existsAddOfLE (α : Type u) [AddGroup α] [LE α] : ExistsAddOfLE α

Equations

• ⋯ = ⋯

@[instance 100]

instance Group.existsMulOfLE (α : Type u) [Group α] [LE α] : ExistsMulOfLE α

Equations

• ⋯ = ⋯

theorem exists_pos_add_of_lt' {α : Type u} [AddZeroClass α] [Preorder α] [ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] [ExistsAddOfLE α] {a : α} {b : α} (h : a < b) : ∃ (c : α), 0 < c ∧ a + c = b

theorem exists_one_lt_mul_of_lt' {α : Type u} [MulOneClass α] [Preorder α] [ContravariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1] [ExistsMulOfLE α] {a : α} {b : α} (h : a < b) : ∃ (c : α), 1 < c ∧ a * c = b

theorem le_of_forall_pos_le_add {α : Type u} [LinearOrder α] [DenselyOrdered α] [AddMonoid α] [ExistsAddOfLE α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] [ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] {a : α} {b : α} (h : ∀ (ε : α), 0 < ε → a ≤ b + ε) : a ≤ b

theorem le_of_forall_one_lt_le_mul {α : Type u} [LinearOrder α] [DenselyOrdered α] [Monoid α] [ExistsMulOfLE α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1] [ContravariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1] {a : α} {b : α} (h : ∀ (ε : α), 1 < ε → a ≤ b * ε) : a ≤ b

theorem le_of_forall_pos_lt_add' {α : Type u} [LinearOrder α] [DenselyOrdered α] [AddMonoid α] [ExistsAddOfLE α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] [ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] {a : α} {b : α} (h : ∀ (ε : α), 0 < ε → a < b + ε) : a ≤ b

theorem le_of_forall_one_lt_lt_mul' {α : Type u} [LinearOrder α] [DenselyOrdered α] [Monoid α] [ExistsMulOfLE α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1] [ContravariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1] {a : α} {b : α} (h : ∀ (ε : α), 1 < ε → a < b * ε) : a ≤ b

theorem le_iff_forall_pos_lt_add' {α : Type u} [LinearOrder α] [DenselyOrdered α] [AddMonoid α] [ExistsAddOfLE α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] [ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] {a : α} {b : α} : a ≤ b ↔ ∀ (ε : α), 0 < ε → a < b + ε

theorem le_iff_forall_one_lt_lt_mul' {α : Type u} [LinearOrder α] [DenselyOrdered α] [Monoid α] [ExistsMulOfLE α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1] [ContravariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1] {a : α} {b : α} : a ≤ b ↔ ∀ (ε : α), 1 < ε → a < b * ε