Adjoining a zero element to an ordered monoid. #

source

ink

class LinearOrderedCommMonoidWithZero (α : Type u_1) extends LinearOrderedCommMonoid , Zero :

Type u_1

Zero is a left absorbing element for multiplication
zero_mul : ∀ (a : α), 0 * a = 0
Zero is a right absorbing element for multiplication
mul_zero : ∀ (a : α), a * 0 = 0
0 ≤ 1≤ 1 in any linearly ordered commutative monoid.
zero_le_one : 0 ≤ 1

A linearly ordered commutative monoid with a zero element.

Instances

source

ink

instance LinearOrderedCommMonoidWithZero.toZeroLeOneClass {α : Type u} [inst : LinearOrderedCommMonoidWithZero α] :

ZeroLEOneClass α

Equations

LinearOrderedCommMonoidWithZero.toZeroLeOneClass = let src := inst; { zero_le_one := (_ : 0 ≤ 1) }

source

ink

instance CanonicallyOrderedAddMonoid.toZeroLeOneClass {α : Type u} [inst : CanonicallyOrderedAddMonoid α] [inst : One α] :

ZeroLEOneClass α

Equations

CanonicallyOrderedAddMonoid.toZeroLeOneClass = { zero_le_one := (_ : 0 ≤ 1) }

source

ink

instance WithZero.preorder {α : Type u} [inst : Preorder α] :

Preorder (WithZero α)

Equations

WithZero.preorder = WithBot.preorder

source

ink

instance WithZero.partialOrder {α : Type u} [inst : PartialOrder α] :

PartialOrder (WithZero α)

Equations

WithZero.partialOrder = WithBot.partialOrder

source

ink

instance WithZero.orderBot {α : Type u} [inst : Preorder α] :

OrderBot (WithZero α)

Equations

WithZero.orderBot = WithBot.orderBot

source

ink

theorem WithZero.zero_le {α : Type u} [inst : Preorder α] (a : WithZero α) :

0 ≤ a

source

ink

theorem WithZero.zero_lt_coe {α : Type u} [inst : Preorder α] (a : α) :

0 < ↑a

source

ink

theorem WithZero.zero_eq_bot {α : Type u} [inst : Preorder α] :

0 = ⊥

source

ink

@[simp]

theorem WithZero.coe_lt_coe {α : Type u} [inst : Preorder α] {a : α} {b : α} :

↑a < ↑b ↔ a < b

source

ink

@[simp]

theorem WithZero.coe_le_coe {α : Type u} [inst : Preorder α] {a : α} {b : α} :

↑a ≤ ↑b ↔ a ≤ b

source

ink

instance WithZero.lattice {α : Type u} [inst : Lattice α] :

Lattice (WithZero α)

Equations

WithZero.lattice = WithBot.lattice

source

ink

instance WithZero.linearOrder {α : Type u} [inst : LinearOrder α] :

LinearOrder (WithZero α)

Equations

WithZero.linearOrder = WithBot.linearOrder

source

ink

instance WithZero.covariantClass_mul_le {α : Type u} [inst : Mul α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] :

CovariantClass (WithZero α) (WithZero α) (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1

Equations

@WithZero.covariantClass_mul_le = @WithZero.covariantClass_mul_le.proof_1

source

ink

instance WithZero.orderedCommMonoid {α : Type u} [inst : OrderedCommMonoid α] :

OrderedCommMonoid (WithZero α)

Equations

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

source

ink

theorem WithZero.covariantClass_add_le {α : Type u} [inst : AddZeroClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (h : ∀ (a : α), 0 ≤ a) :

CovariantClass (WithZero α) (WithZero α) (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

source

ink

def WithZero.orderedAddCommMonoid {α : Type u} [inst : OrderedAddCommMonoid α] (zero_le : ∀ (a : α), 0 ≤ a) :

OrderedAddCommMonoid (WithZero α)

If 0 is the least element in α, then WithZero α is an OrderedAddCommMonoid. See note [reducible non-instances].

Equations

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

source

ink

instance WithZero.existsAddOfLE {α : Type u} [inst : Add α] [inst : Preorder α] [inst : ExistsAddOfLE α] :

ExistsAddOfLE (WithZero α)

Equations

@WithZero.existsAddOfLE = @WithZero.existsAddOfLE.proof_1

source

ink

instance WithZero.canonicallyOrderedAddMonoid {α : Type u} [inst : CanonicallyOrderedAddMonoid α] :

CanonicallyOrderedAddMonoid (WithZero α)

Adding a new zero to a canonically ordered additive monoid produces another one.

Equations

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

source

ink

instance WithZero.canonicallyLinearOrderedAddMonoid (α : Type u_1) [inst : CanonicallyLinearOrderedAddMonoid α] :

CanonicallyLinearOrderedAddMonoid (WithZero α)

Equations

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