Documentation

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

Prop

For a ≤ b≤ b, there is a c so b = a + c.
exists_add_of_le : ∀ {a b : α}, a ≤ b → ∃ c, b = a + c

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

Instances

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

Equations

AddGroup.existsAddOfLE = AddGroup.existsAddOfLE.proof_1

def AddGroup.existsAddOfLE.proof_1 (α : Type u_1) [inst : AddGroup α] [inst : LE α] :

Equations

(_ : ExistsAddOfLE α) = (_ : ExistsAddOfLE α)

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

ExistsMulOfLE α

Equations

Group.existsMulOfLE = Group.existsMulOfLE.proof_1

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

∃ c, 0 < c ∧ a + c = b

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

∃ c, 1 < c ∧ a * c = b

theorem le_of_forall_pos_le_add {α : Type u} [inst : LinearOrder α] [inst : DenselyOrdered α] [inst : AddMonoid α] [inst : ExistsAddOfLE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : 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} [inst : LinearOrder α] [inst : DenselyOrdered α] [inst : Monoid α] [inst : ExistsMulOfLE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : 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} [inst : LinearOrder α] [inst : DenselyOrdered α] [inst : AddMonoid α] [inst : ExistsAddOfLE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : 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} [inst : LinearOrder α] [inst : DenselyOrdered α] [inst : Monoid α] [inst : ExistsMulOfLE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : 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} [inst : LinearOrder α] [inst : DenselyOrdered α] [inst : AddMonoid α] [inst : ExistsAddOfLE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : 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} [inst : LinearOrder α] [inst : DenselyOrdered α] [inst : Monoid α] [inst : ExistsMulOfLE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} :

a ≤ b ↔ ∀ (ε : α), 1 < ε → a < b * ε

class CanonicallyOrderedAddMonoid (α : Type u_1) extends OrderedAddCommMonoid , Bot :

Type u_1

⊥⊥ is the least element
bot_le : ∀ (x : α), ⊥ ≤ x
For a ≤ b≤ b, there is a c so b = a + c.
exists_add_of_le : ∀ {a b : α}, a ≤ b → ∃ c, b = a + c
For any a and b, a ≤ a + b≤ a + b
le_self_add : ∀ (a b : α), a ≤ a + b

A canonically ordered additive monoid is an ordered commutative additive monoid in which the ordering coincides with the subtractibility relation, which is to say, a ≤ b≤ b iff there exists c with b = a + c. This is satisfied by the natural numbers, for example, but not the integers or other nontrivial OrderedAddCommGroups.

Instances

instance CanonicallyOrderedAddMonoid.toOrderBot (α : Type u) [h : CanonicallyOrderedAddMonoid α] :

OrderBot α

Equations

CanonicallyOrderedAddMonoid.toOrderBot α = OrderBot.mk (_ : ∀ (x : α), ⊥ ≤ x)

class CanonicallyOrderedMonoid (α : Type u_1) extends OrderedCommMonoid , Bot :

Type u_1

⊥⊥ is the least element
bot_le : ∀ (x : α), ⊥ ≤ x
For a ≤ b≤ b, there is a c so b = a * c.
exists_mul_of_le : ∀ {a b : α}, a ≤ b → ∃ c, b = a * c
For any a and b, a ≤ a * b≤ a * b
le_self_mul : ∀ (a b : α), a ≤ a * b

A canonically ordered monoid is an ordered commutative monoid in which the ordering coincides with the divisibility relation, which is to say, a ≤ b≤ b iff there exists c with b = a * c. Examples seem rare; it seems more likely that the OrderDual of a naturally-occurring lattice satisfies this than the lattice itself (for example, dual of the lattice of ideals of a PID or Dedekind domain satisfy this; collections of all things ≤ 1 seem to be more natural that collections of all things ≥ 1).

Instances

instance CanonicallyOrderedMonoid.toOrderBot (α : Type u) [h : CanonicallyOrderedMonoid α] :

OrderBot α

Equations

CanonicallyOrderedMonoid.toOrderBot α = OrderBot.mk (_ : ∀ (x : α), ⊥ ≤ x)

def CanonicallyOrderedAddMonoid.existsAddOfLE.proof_1 (α : Type u_1) [h : CanonicallyOrderedAddMonoid α] :

Equations

(_ : ExistsAddOfLE α) = (_ : ExistsAddOfLE α)

instance CanonicallyOrderedAddMonoid.existsAddOfLE (α : Type u) [h : CanonicallyOrderedAddMonoid α] :

Equations

CanonicallyOrderedAddMonoid.existsAddOfLE = CanonicallyOrderedAddMonoid.existsAddOfLE.proof_1

instance CanonicallyOrderedMonoid.existsMulOfLE (α : Type u) [h : CanonicallyOrderedMonoid α] :

ExistsMulOfLE α

Equations

CanonicallyOrderedMonoid.existsMulOfLE = CanonicallyOrderedMonoid.existsMulOfLE.proof_1

theorem le_self_add {α : Type u} [inst : CanonicallyOrderedAddMonoid α] {a : α} {c : α} :

a ≤ a + c

theorem le_self_mul {α : Type u} [inst : CanonicallyOrderedMonoid α] {a : α} {c : α} :

a ≤ a * c

theorem le_add_self {α : Type u} [inst : CanonicallyOrderedAddMonoid α] {a : α} {b : α} :

a ≤ b + a

theorem le_mul_self {α : Type u} [inst : CanonicallyOrderedMonoid α] {a : α} {b : α} :

a ≤ b * a

@[simp]

theorem self_le_add_right {α : Type u} [inst : CanonicallyOrderedAddMonoid α] (a : α) (b : α) :

a ≤ a + b

@[simp]

theorem self_le_mul_right {α : Type u} [inst : CanonicallyOrderedMonoid α] (a : α) (b : α) :

a ≤ a * b

@[simp]

theorem self_le_add_left {α : Type u} [inst : CanonicallyOrderedAddMonoid α] (a : α) (b : α) :

a ≤ b + a

@[simp]

theorem self_le_mul_left {α : Type u} [inst : CanonicallyOrderedMonoid α] (a : α) (b : α) :

a ≤ b * a

theorem le_of_add_le_left {α : Type u} [inst : CanonicallyOrderedAddMonoid α] {a : α} {b : α} {c : α} :

a + b ≤ c → a ≤ c

theorem le_of_mul_le_left {α : Type u} [inst : CanonicallyOrderedMonoid α] {a : α} {b : α} {c : α} :

a * b ≤ c → a ≤ c

theorem le_of_add_le_right {α : Type u} [inst : CanonicallyOrderedAddMonoid α] {a : α} {b : α} {c : α} :

a + b ≤ c → b ≤ c

theorem le_of_mul_le_right {α : Type u} [inst : CanonicallyOrderedMonoid α] {a : α} {b : α} {c : α} :

a * b ≤ c → b ≤ c

theorem le_iff_exists_add {α : Type u} [inst : CanonicallyOrderedAddMonoid α] {a : α} {b : α} :

a ≤ b ↔ ∃ c, b = a + c

theorem le_iff_exists_mul {α : Type u} [inst : CanonicallyOrderedMonoid α] {a : α} {b : α} :

a ≤ b ↔ ∃ c, b = a * c

theorem le_iff_exists_add' {α : Type u} [inst : CanonicallyOrderedAddMonoid α] {a : α} {b : α} :

a ≤ b ↔ ∃ c, b = c + a

theorem le_iff_exists_mul' {α : Type u} [inst : CanonicallyOrderedMonoid α] {a : α} {b : α} :

a ≤ b ↔ ∃ c, b = c * a

@[simp]

theorem zero_le {α : Type u} [inst : CanonicallyOrderedAddMonoid α] (a : α) :

0 ≤ a

@[simp]

theorem one_le {α : Type u} [inst : CanonicallyOrderedMonoid α] (a : α) :

1 ≤ a

theorem bot_eq_zero {α : Type u} [inst : CanonicallyOrderedAddMonoid α] :

⊥ = 0

theorem bot_eq_one {α : Type u} [inst : CanonicallyOrderedMonoid α] :

⊥ = 1

@[simp]

theorem add_eq_zero_iff {α : Type u} [inst : CanonicallyOrderedAddMonoid α] {a : α} {b : α} :

a + b = 0 ↔ a = 0 ∧ b = 0

@[simp]

theorem mul_eq_one_iff {α : Type u} [inst : CanonicallyOrderedMonoid α] {a : α} {b : α} :

a * b = 1 ↔ a = 1 ∧ b = 1

@[simp]

theorem nonpos_iff_eq_zero {α : Type u} [inst : CanonicallyOrderedAddMonoid α] {a : α} :

a ≤ 0 ↔ a = 0

@[simp]

theorem le_one_iff_eq_one {α : Type u} [inst : CanonicallyOrderedMonoid α] {a : α} :

a ≤ 1 ↔ a = 1

theorem pos_iff_ne_zero {α : Type u} [inst : CanonicallyOrderedAddMonoid α] {a : α} :

0 < a ↔ a ≠ 0

theorem one_lt_iff_ne_one {α : Type u} [inst : CanonicallyOrderedMonoid α] {a : α} :

1 < a ↔ a ≠ 1

theorem eq_zero_or_pos {α : Type u} [inst : CanonicallyOrderedAddMonoid α] {a : α} :

a = 0 ∨ 0 < a

theorem eq_one_or_one_lt {α : Type u} [inst : CanonicallyOrderedMonoid α] {a : α} :

a = 1 ∨ 1 < a

@[simp]

theorem add_pos_iff {α : Type u} [inst : CanonicallyOrderedAddMonoid α] {a : α} {b : α} :

0 < a + b ↔ 0 < a ∨ 0 < b

@[simp]

theorem one_lt_mul_iff {α : Type u} [inst : CanonicallyOrderedMonoid α] {a : α} {b : α} :

1 < a * b ↔ 1 < a ∨ 1 < b

theorem exists_pos_add_of_lt {α : Type u} [inst : CanonicallyOrderedAddMonoid α] {a : α} {b : α} (h : a < b) :

∃ c x, a + c = b

theorem exists_one_lt_mul_of_lt {α : Type u} [inst : CanonicallyOrderedMonoid α] {a : α} {b : α} (h : a < b) :

∃ c x, a * c = b

theorem le_add_left {α : Type u} [inst : CanonicallyOrderedAddMonoid α] {a : α} {b : α} {c : α} (h : a ≤ c) :

a ≤ b + c

theorem le_mul_left {α : Type u} [inst : CanonicallyOrderedMonoid α] {a : α} {b : α} {c : α} (h : a ≤ c) :

a ≤ b * c

theorem le_add_right {α : Type u} [inst : CanonicallyOrderedAddMonoid α] {a : α} {b : α} {c : α} (h : a ≤ b) :

a ≤ b + c

theorem le_mul_right {α : Type u} [inst : CanonicallyOrderedMonoid α] {a : α} {b : α} {c : α} (h : a ≤ b) :

a ≤ b * c

theorem lt_iff_exists_add {α : Type u} [inst : CanonicallyOrderedAddMonoid α] {a : α} {b : α} [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] :

a < b ↔ ∃ c, c > 0 ∧ b = a + c

theorem lt_iff_exists_mul {α : Type u} [inst : CanonicallyOrderedMonoid α] {a : α} {b : α} [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] :

a < b ↔ ∃ c, c > 1 ∧ b = a * c

theorem pos_of_gt {M : Type u_1} [inst : CanonicallyOrderedAddMonoid M] {n : M} {m : M} (h : n < m) :

0 < m

theorem NeZero.pos {M : Type u_1} (a : M) [inst : CanonicallyOrderedAddMonoid M] [inst : NeZero a] :

0 < a

theorem NeZero.of_gt {M : Type u_1} [inst : CanonicallyOrderedAddMonoid M] {x : M} {y : M} (h : x < y) :

NeZero y

instance NeZero.of_gt' {M : Type u_1} [inst : CanonicallyOrderedAddMonoid M] [inst : One M] {y : M} [inst : Fact (1 < y)] :

NeZero y

Equations

@NeZero.of_gt' = @NeZero.of_gt'.proof_1

instance NeZero.bit0 {M : Type u_1} [inst : CanonicallyOrderedAddMonoid M] {x : M} [inst : NeZero x] :

NeZero (bit0 x)

Equations

@NeZero.bit0 = @NeZero.bit0.proof_1

class CanonicallyLinearOrderedAddMonoid (α : Type u_1) extends CanonicallyOrderedAddMonoid , Min , Max :

Type u_1

A linear order is total.
le_total : ∀ (a b : α), a ≤ b ∨ b ≤ a
In a linearly ordered type, we assume the order relations are all decidable.
decidable_le : DecidableRel fun x x_1 => x ≤ x_1
In a linearly ordered type, we assume the order relations are all decidable.
decidable_eq : DecidableEq α
In a linearly ordered type, we assume the order relations are all decidable.
decidable_lt : DecidableRel fun x x_1 => x < x_1
The minimum function is equivalent to the one you get from minOfLe.
min_def : autoParam (∀ (a b : α), min a b = if a ≤ b then a else b) _auto✝
The minimum function is equivalent to the one you get from maxOfLe.
max_def : autoParam (∀ (a b : α), max a b = if a ≤ b then b else a) _auto✝

A canonically linear-ordered additive monoid is a canonically ordered additive monoid whose ordering is a linear order.

Instances

class CanonicallyLinearOrderedMonoid (α : Type u_1) extends CanonicallyOrderedMonoid , Min , Max :

Type u_1

A linear order is total.
le_total : ∀ (a b : α), a ≤ b ∨ b ≤ a
In a linearly ordered type, we assume the order relations are all decidable.
decidable_le : DecidableRel fun x x_1 => x ≤ x_1
In a linearly ordered type, we assume the order relations are all decidable.
decidable_eq : DecidableEq α
In a linearly ordered type, we assume the order relations are all decidable.
decidable_lt : DecidableRel fun x x_1 => x < x_1
The minimum function is equivalent to the one you get from minOfLe.
min_def : autoParam (∀ (a b : α), min a b = if a ≤ b then a else b) _auto✝
The minimum function is equivalent to the one you get from maxOfLe.
max_def : autoParam (∀ (a b : α), max a b = if a ≤ b then b else a) _auto✝

A canonically linear-ordered monoid is a canonically ordered monoid whose ordering is a linear order.

Instances

def CanonicallyLinearOrderedAddMonoid.semilatticeSup.proof_2 {α : Type u_1} [inst : CanonicallyLinearOrderedAddMonoid α] (a : α) (b : α) :

b ≤ a ⊔ b

Equations

(_ : ∀ (a b : α), b ≤ a ⊔ b) = (_ : ∀ (a b : α), b ≤ a ⊔ b)

instance CanonicallyLinearOrderedAddMonoid.semilatticeSup {α : Type u} [inst : CanonicallyLinearOrderedAddMonoid α] :

SemilatticeSup α

Equations

One or more equations did not get rendered due to their size.

def CanonicallyLinearOrderedAddMonoid.semilatticeSup.proof_3 {α : Type u_1} [inst : CanonicallyLinearOrderedAddMonoid α] (a : α) (b : α) (c : α) :

a ≤ c → b ≤ c → a ⊔ b ≤ c

Equations

(_ : ∀ (a b c : α), a ≤ c → b ≤ c → a ⊔ b ≤ c) = (_ : ∀ (a b c : α), a ≤ c → b ≤ c → a ⊔ b ≤ c)

def CanonicallyLinearOrderedAddMonoid.semilatticeSup.proof_1 {α : Type u_1} [inst : CanonicallyLinearOrderedAddMonoid α] (a : α) (b : α) :

a ≤ a ⊔ b

Equations

(_ : ∀ (a b : α), a ≤ a ⊔ b) = (_ : ∀ (a b : α), a ≤ a ⊔ b)

instance CanonicallyLinearOrderedMonoid.semilatticeSup {α : Type u} [inst : CanonicallyLinearOrderedMonoid α] :

SemilatticeSup α

Equations

One or more equations did not get rendered due to their size.

theorem min_add_distrib {α : Type u} [inst : CanonicallyLinearOrderedAddMonoid α] (a : α) (b : α) (c : α) :

min a (b + c) = min a (min a b + min a c)

theorem min_mul_distrib {α : Type u} [inst : CanonicallyLinearOrderedMonoid α] (a : α) (b : α) (c : α) :

min a (b * c) = min a (min a b * min a c)

theorem min_add_distrib' {α : Type u} [inst : CanonicallyLinearOrderedAddMonoid α] (a : α) (b : α) (c : α) :

min (a + b) c = min (min a c + min b c) c

theorem min_mul_distrib' {α : Type u} [inst : CanonicallyLinearOrderedMonoid α] (a : α) (b : α) (c : α) :

min (a * b) c = min (min a c * min b c) c

theorem zero_min {α : Type u} [inst : CanonicallyLinearOrderedAddMonoid α] (a : α) :

min 0 a = 0

theorem one_min {α : Type u} [inst : CanonicallyLinearOrderedMonoid α] (a : α) :

min 1 a = 1

theorem min_zero {α : Type u} [inst : CanonicallyLinearOrderedAddMonoid α] (a : α) :

min a 0 = 0

theorem min_one {α : Type u} [inst : CanonicallyLinearOrderedMonoid α] (a : α) :

min a 1 = 1

@[simp]

theorem bot_eq_zero' {α : Type u} [inst : CanonicallyLinearOrderedAddMonoid α] :

⊥ = 0

In a linearly ordered monoid, we are happy for bot_eq_zero to be a @[simp] lemma