Unbundled and weaker forms of canonically ordered monoids #
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
.
For
a ≤ b
,a
left dividesb
Instances
theorem
ExistsMulOfLE.exists_mul_of_le
{α : Type u}
[Mul α]
[LE α]
[self : ExistsMulOfLE α]
{a : α}
{b : α}
:
For a ≤ b
, a
left divides b
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
.
For
a ≤ b
, there is ac
sob = a + c
.
Instances
theorem
ExistsAddOfLE.exists_add_of_le
{α : Type u}
[Add α]
[LE α]
[self : ExistsAddOfLE α]
{a : α}
{b : α}
:
For a ≤ b
, there is a c
so b = a + c
.
@[instance 100]
Equations
- ⋯ = ⋯
@[instance 100]
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)
:
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)
:
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 : α}
:
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 : α}
: