Adjoining top/bottom elements to ordered monoids.

instance WithTop.zero {α : Type u} [Zero α] : Zero (WithTop α)

Equations

• WithTop.zero = { zero := ↑0 }

instance WithTop.one {α : Type u} [One α] : One (WithTop α)

Equations

• WithTop.one = { one := ↑1 }

@[simp]

theorem WithTop.coe_zero {α : Type u} [Zero α] : ↑0 = 0

@[simp]

theorem WithTop.coe_one {α : Type u} [One α] : ↑1 = 1

@[simp]

theorem WithTop.coe_eq_zero {α : Type u} [Zero α] {a : α} : ↑a = 0 ↔ a = 0

@[simp]

theorem WithTop.coe_eq_one {α : Type u} [One α] {a : α} : ↑a = 1 ↔ a = 1

@[simp]

theorem WithTop.untop_zero {α : Type u} [Zero α] : WithTop.untop 0 (_ : ↑0 ≠ ⊤) = 0

@[simp]

theorem WithTop.untop_one {α : Type u} [One α] : WithTop.untop 1 (_ : ↑1 ≠ ⊤) = 1

@[simp]

theorem WithTop.untop_zero' {α : Type u} [Zero α] (d : α) : WithTop.untop' d 0 = 0

@[simp]

theorem WithTop.untop_one' {α : Type u} [One α] (d : α) : WithTop.untop' d 1 = 1

@[simp]

theorem WithTop.coe_nonneg {α : Type u} [Zero α] [LE α] {a : α} : 0 ≤ ↑a ↔ 0 ≤ a

@[simp]

theorem WithTop.one_le_coe {α : Type u} [One α] [LE α] {a : α} : 1 ≤ ↑a ↔ 1 ≤ a

@[simp]

theorem WithTop.coe_le_zero {α : Type u} [Zero α] [LE α] {a : α} : ↑a ≤ 0 ↔ a ≤ 0

@[simp]

theorem WithTop.coe_le_one {α : Type u} [One α] [LE α] {a : α} : ↑a ≤ 1 ↔ a ≤ 1

@[simp]

theorem WithTop.coe_pos {α : Type u} [Zero α] [LT α] {a : α} : 0 < ↑a ↔ 0 < a

@[simp]

theorem WithTop.one_lt_coe {α : Type u} [One α] [LT α] {a : α} : 1 < ↑a ↔ 1 < a

@[simp]

theorem WithTop.coe_lt_zero {α : Type u} [Zero α] [LT α] {a : α} : ↑a < 0 ↔ a < 0

@[simp]

theorem WithTop.coe_lt_one {α : Type u} [One α] [LT α] {a : α} : ↑a < 1 ↔ a < 1

@[simp]

theorem WithTop.map_zero {α : Type u} [Zero α] {β : Type u_1} (f : α → β) : WithTop.map f 0 = ↑(f 0)

@[simp]

theorem WithTop.map_one {α : Type u} [One α] {β : Type u_1} (f : α → β) : WithTop.map f 1 = ↑(f 1)

@[simp]

theorem WithTop.zero_eq_coe {α : Type u} [Zero α] {a : α} : 0 = ↑a ↔ a = 0

@[simp]

theorem WithTop.one_eq_coe {α : Type u} [One α] {a : α} : 1 = ↑a ↔ a = 1

@[simp]

theorem WithTop.top_ne_zero {α : Type u} [Zero α] : ⊤ ≠ 0

abbrev WithTop.top_ne_zero.match_1 {α : Type u_1} [Zero α] (motive : ⊤ = 0 → Prop) : (a : ⊤ = 0) → motive a

Equations

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

@[simp]

theorem WithTop.top_ne_one {α : Type u} [One α] : ⊤ ≠ 1

@[simp]

theorem WithTop.zero_ne_top {α : Type u} [Zero α] : 0 ≠ ⊤

abbrev WithTop.zero_ne_top.match_1 {α : Type u_1} [Zero α] (motive : 0 = ⊤ → Prop) : (a : 0 = ⊤) → motive a

Equations

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

@[simp]

theorem WithTop.one_ne_top {α : Type u} [One α] : 1 ≠ ⊤

instance WithTop.zeroLEOneClass {α : Type u} [One α] [Zero α] [LE α] [ZeroLEOneClass α] : ZeroLEOneClass (WithTop α)

Equations

• @WithTop.zeroLEOneClass = @WithTop.zeroLEOneClass.proof_1

instance WithTop.add {α : Type u} [Add α] : Add (WithTop α)

Equations

• WithTop.add = { add := Option.map₂ fun x x_1 => x + x_1 }

theorem WithTop.coe_add {α : Type u} [Add α] {x : α} {y : α} : ↑(x + y) = ↑x + ↑y

@[deprecated]

theorem WithTop.coe_bit0 {α : Type u} [Add α] {x : α} : ↑(bit0 x) = bit0 ↑x

@[deprecated]

theorem WithTop.coe_bit1 {α : Type u} [Add α] [One α] {a : α} : ↑(bit1 a) = bit1 ↑a

@[simp]

theorem WithTop.top_add {α : Type u} [Add α] (a : WithTop α) : ⊤ + a = ⊤

@[simp]

theorem WithTop.add_top {α : Type u} [Add α] (a : WithTop α) : a + ⊤ = ⊤

@[simp]

theorem WithTop.add_eq_top {α : Type u} [Add α] {a : WithTop α} {b : WithTop α} : a + b = ⊤ ↔ a = ⊤ ∨ b = ⊤

theorem WithTop.add_ne_top {α : Type u} [Add α] {a : WithTop α} {b : WithTop α} : a + b ≠ ⊤ ↔ a ≠ ⊤ ∧ b ≠ ⊤

theorem WithTop.add_lt_top {α : Type u} [Add α] [LT α] {a : WithTop α} {b : WithTop α} : a + b < ⊤ ↔ a < ⊤ ∧ b < ⊤

theorem WithTop.add_eq_coe {α : Type u} [Add α] {a : WithTop α} {b : WithTop α} {c : α} : a + b = ↑c ↔ ∃ a' b', ↑a' = a ∧ ↑b' = b ∧ a' + b' = c

theorem WithTop.add_coe_eq_top_iff {α : Type u} [Add α] {x : WithTop α} {y : α} : x + ↑y = ⊤ ↔ x = ⊤

theorem WithTop.coe_add_eq_top_iff {α : Type u} [Add α] {x : α} {y : WithTop α} : ↑x + y = ⊤ ↔ y = ⊤

theorem WithTop.add_right_cancel_iff {α : Type u} [Add α] {a : WithTop α} {b : WithTop α} {c : WithTop α} [IsRightCancelAdd α] (ha : a ≠ ⊤) : b + a = c + a ↔ b = c

theorem WithTop.add_right_cancel {α : Type u} [Add α] {a : WithTop α} {b : WithTop α} {c : WithTop α} [IsRightCancelAdd α] (ha : a ≠ ⊤) (h : b + a = c + a) : b = c

theorem WithTop.add_left_cancel_iff {α : Type u} [Add α] {a : WithTop α} {b : WithTop α} {c : WithTop α} [IsLeftCancelAdd α] (ha : a ≠ ⊤) : a + b = a + c ↔ b = c

theorem WithTop.add_left_cancel {α : Type u} [Add α] {a : WithTop α} {b : WithTop α} {c : WithTop α} [IsLeftCancelAdd α] (ha : a ≠ ⊤) (h : a + b = a + c) : b = c

instance WithTop.covariantClass_add_le {α : Type u} [Add α] [LE α] [CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] : CovariantClass (WithTop α) (WithTop α) (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

Equations

• @WithTop.covariantClass_add_le = @WithTop.covariantClass_add_le.proof_1

instance WithTop.covariantClass_swap_add_le {α : Type u} [Add α] [LE α] [CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] : CovariantClass (WithTop α) (WithTop α) (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

Equations

• @WithTop.covariantClass_swap_add_le = @WithTop.covariantClass_swap_add_le.proof_1

instance WithTop.contravariantClass_add_lt {α : Type u} [Add α] [LT α] [ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] : ContravariantClass (WithTop α) (WithTop α) (fun x x_1 => x + x_1) fun x x_1 => x < x_1

Equations

• @WithTop.contravariantClass_add_lt = @WithTop.contravariantClass_add_lt.proof_1

instance WithTop.contravariantClass_swap_add_lt {α : Type u} [Add α] [LT α] [ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] : ContravariantClass (WithTop α) (WithTop α) (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1

Equations

• @WithTop.contravariantClass_swap_add_lt = @WithTop.contravariantClass_swap_add_lt.proof_1

theorem WithTop.le_of_add_le_add_left {α : Type u} [Add α] {a : WithTop α} {b : WithTop α} {c : WithTop α} [LE α] [ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (ha : a ≠ ⊤) (h : a + b ≤ a + c) : b ≤ c

theorem WithTop.le_of_add_le_add_right {α : Type u} [Add α] {a : WithTop α} {b : WithTop α} {c : WithTop α} [LE α] [ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (ha : a ≠ ⊤) (h : b + a ≤ c + a) : b ≤ c

theorem WithTop.add_lt_add_left {α : Type u} [Add α] {a : WithTop α} {b : WithTop α} {c : WithTop α} [LT α] [CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] (ha : a ≠ ⊤) (h : b < c) : a + b < a + c

theorem WithTop.add_lt_add_right {α : Type u} [Add α] {a : WithTop α} {b : WithTop α} {c : WithTop α} [LT α] [CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] (ha : a ≠ ⊤) (h : b < c) : b + a < c + a

theorem WithTop.add_le_add_iff_left {α : Type u} [Add α] {a : WithTop α} {b : WithTop α} {c : WithTop α} [LE α] [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] (ha : a ≠ ⊤) : a + b ≤ a + c ↔ b ≤ c

theorem WithTop.add_le_add_iff_right {α : Type u} [Add α] {a : WithTop α} {b : WithTop α} {c : WithTop α} [LE α] [CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (ha : a ≠ ⊤) : b + a ≤ c + a ↔ b ≤ c

theorem WithTop.add_lt_add_iff_left {α : Type u} [Add α] {a : WithTop α} {b : WithTop α} {c : WithTop α} [LT α] [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] (ha : a ≠ ⊤) : a + b < a + c ↔ b < c

theorem WithTop.add_lt_add_iff_right {α : Type u} [Add α] {a : WithTop α} {b : WithTop α} {c : WithTop α} [LT α] [CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] [ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] (ha : a ≠ ⊤) : b + a < c + a ↔ b < c

theorem WithTop.add_lt_add_of_le_of_lt {α : Type u} [Add α] {a : WithTop α} {b : WithTop α} {c : WithTop α} {d : WithTop α} [Preorder α] [CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (ha : a ≠ ⊤) (hab : a ≤ b) (hcd : c < d) : a + c < b + d

theorem WithTop.add_lt_add_of_lt_of_le {α : Type u} [Add α] {a : WithTop α} {b : WithTop α} {c : WithTop α} {d : WithTop α} [Preorder α] [CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] (hc : c ≠ ⊤) (hab : a < b) (hcd : c ≤ d) : a + c < b + d

@[simp]

theorem WithTop.map_add {α : Type u} {β : Type v} [Add α] {F : Type u_1} [Add β] [AddHomClass F α β] (f : F) (a : WithTop α) (b : WithTop α) : WithTop.map (↑f) (a + b) = WithTop.map (↑f) a + WithTop.map (↑f) b

instance WithTop.addSemigroup {α : Type u} [AddSemigroup α] : AddSemigroup (WithTop α)

Equations

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

instance WithTop.addCommSemigroup {α : Type u} [AddCommSemigroup α] : AddCommSemigroup (WithTop α)

Equations

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

instance WithTop.addZeroClass {α : Type u} [AddZeroClass α] : AddZeroClass (WithTop α)

Equations

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

instance WithTop.addMonoid {α : Type u} [AddMonoid α] : AddMonoid (WithTop α)

Equations

• WithTop.addMonoid = let src := WithTop.addSemigroup; let src_1 := WithTop.addZeroClass; AddMonoid.mk (_ : ∀ (a : WithTop α), 0 + a = a) (_ : ∀ (a : WithTop α), a + 0 = a) nsmulRec

instance WithTop.addCommMonoid {α : Type u} [AddCommMonoid α] : AddCommMonoid (WithTop α)

Equations

• WithTop.addCommMonoid = let src := WithTop.addMonoid; let src_1 := WithTop.addCommSemigroup; AddCommMonoid.mk (_ : ∀ (a b : WithTop α), a + b = b + a)

instance WithTop.addMonoidWithOne {α : Type u} [AddMonoidWithOne α] : AddMonoidWithOne (WithTop α)

Equations

• WithTop.addMonoidWithOne = let src := WithTop.one; let src_1 := WithTop.addMonoid; AddMonoidWithOne.mk

instance WithTop.charZero {α : Type u} [AddMonoidWithOne α] [CharZero α] : CharZero (WithTop α)

Equations

• @WithTop.charZero = @WithTop.charZero.proof_1

instance WithTop.addCommMonoidWithOne {α : Type u} [AddCommMonoidWithOne α] : AddCommMonoidWithOne (WithTop α)

Equations

• WithTop.addCommMonoidWithOne = let src := WithTop.addMonoidWithOne; let src_1 := WithTop.addCommMonoid; AddCommMonoidWithOne.mk (_ : ∀ (a b : WithTop α), a + b = b + a)

instance WithTop.orderedAddCommMonoid {α : Type u} [OrderedAddCommMonoid α] : OrderedAddCommMonoid (WithTop α)

Equations

• WithTop.orderedAddCommMonoid = let src := WithTop.partialOrder; let src_1 := WithTop.addCommMonoid; OrderedAddCommMonoid.mk (_ : ∀ (a b : WithTop α), a ≤ b → ∀ (c : WithTop α), c + a ≤ c + b)

instance WithTop.linearOrderedAddCommMonoidWithTop {α : Type u} [LinearOrderedAddCommMonoid α] : LinearOrderedAddCommMonoidWithTop (WithTop α)

Equations

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

instance WithTop.existsAddOfLE {α : Type u} [LE α] [Add α] [ExistsAddOfLE α] : ExistsAddOfLE (WithTop α)

Equations

• @WithTop.existsAddOfLE = @WithTop.existsAddOfLE.proof_1

instance WithTop.canonicallyOrderedAddMonoid {α : Type u} [CanonicallyOrderedAddMonoid α] : CanonicallyOrderedAddMonoid (WithTop α)

Equations

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

instance WithTop.instCanonicallyLinearOrderedAddMonoidWithTop {α : Type u} [CanonicallyLinearOrderedAddMonoid α] : CanonicallyLinearOrderedAddMonoid (WithTop α)

Equations

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

@[simp]

theorem WithTop.coe_nat {α : Type u} [AddMonoidWithOne α] (n : ℕ) : ↑↑n = ↑n

@[simp]

theorem WithTop.nat_ne_top {α : Type u} [AddMonoidWithOne α] (n : ℕ) : ↑n ≠ ⊤

@[simp]

theorem WithTop.top_ne_nat {α : Type u} [AddMonoidWithOne α] (n : ℕ) : ⊤ ≠ ↑n

def WithTop.addHom {α : Type u} [AddMonoid α] : α →+ WithTop α

Coercion from α to WithTop α as an AddMonoidHom.

Equations

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

@[simp]

theorem WithTop.zero_lt_top {α : Type u} [OrderedAddCommMonoid α] : 0 < ⊤

theorem WithTop.zero_lt_coe {α : Type u} [OrderedAddCommMonoid α] (a : α) : 0 < ↑a ↔ 0 < a

def ZeroHom.withTopMap {M : Type u_1} {N : Type u_2} [Zero M] [Zero N] (f : ZeroHom M N) : ZeroHom (WithTop M) (WithTop N)

A version of WithTop.map for ZeroHoms

Equations

• ZeroHom.withTopMap f = { toFun := WithTop.map ↑f, map_zero' := (_ : WithTop.map (↑f) 0 = 0) }

theorem ZeroHom.withTopMap.proof_1 {M : Type u_2} {N : Type u_1} [Zero M] [Zero N] (f : ZeroHom M N) : WithTop.map (↑f) 0 = 0

@[simp]

theorem ZeroHom.withTopMap_apply {M : Type u_1} {N : Type u_2} [Zero M] [Zero N] (f : ZeroHom M N) : ↑(ZeroHom.withTopMap f) = WithTop.map ↑f

@[simp]

theorem OneHom.withTopMap_apply {M : Type u_1} {N : Type u_2} [One M] [One N] (f : OneHom M N) : ↑(OneHom.withTopMap f) = WithTop.map ↑f

def OneHom.withTopMap {M : Type u_1} {N : Type u_2} [One M] [One N] (f : OneHom M N) : OneHom (WithTop M) (WithTop N)

A version of WithTop.map for OneHoms.

Equations

• OneHom.withTopMap f = { toFun := WithTop.map ↑f, map_one' := (_ : WithTop.map (↑f) 1 = 1) }

@[simp]

theorem AddHom.withTopMap_apply {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) : ↑(AddHom.withTopMap f) = WithTop.map ↑f

def AddHom.withTopMap {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) : AddHom (WithTop M) (WithTop N)

A version of WithTop.map for AddHoms.

Equations

• AddHom.withTopMap f = { toFun := WithTop.map ↑f, map_add' := (_ : ∀ (a b : WithTop M), WithTop.map (↑f) (a + b) = WithTop.map (↑f) a + WithTop.map (↑f) b) }

@[simp]

theorem AddMonoidHom.withTopMap_apply {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) : ↑(AddMonoidHom.withTopMap f) = WithTop.map ↑f

def AddMonoidHom.withTopMap {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) : WithTop M →+ WithTop N

A version of WithTop.map for AddMonoidHoms.

Equations

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

instance WithBot.zero {α : Type u} [Zero α] : Zero (WithBot α)

Equations

• WithBot.zero = WithTop.zero

instance WithBot.one {α : Type u} [One α] : One (WithBot α)

Equations

• WithBot.one = WithTop.one

instance WithBot.add {α : Type u} [Add α] : Add (WithBot α)

Equations

• WithBot.add = WithTop.add

instance WithBot.AddSemigroup {α : Type u} [AddSemigroup α] : AddSemigroup (WithBot α)

Equations

• WithBot.AddSemigroup = WithTop.addSemigroup

instance WithBot.addCommSemigroup {α : Type u} [AddCommSemigroup α] : AddCommSemigroup (WithBot α)

Equations

• WithBot.addCommSemigroup = WithTop.addCommSemigroup

instance WithBot.addZeroClass {α : Type u} [AddZeroClass α] : AddZeroClass (WithBot α)

Equations

• WithBot.addZeroClass = WithTop.addZeroClass

instance WithBot.addMonoid {α : Type u} [AddMonoid α] : AddMonoid (WithBot α)

Equations

• WithBot.addMonoid = WithTop.addMonoid

instance WithBot.addCommMonoid {α : Type u} [AddCommMonoid α] : AddCommMonoid (WithBot α)

Equations

• WithBot.addCommMonoid = WithTop.addCommMonoid

instance WithBot.addMonoidWithOne {α : Type u} [AddMonoidWithOne α] : AddMonoidWithOne (WithBot α)

Equations

• WithBot.addMonoidWithOne = WithTop.addMonoidWithOne

instance WithBot.charZero {α : Type u} [AddMonoidWithOne α] [CharZero α] : CharZero (WithBot α)

Equations

• (_ : CharZero (WithBot α)) = (_ : CharZero (WithTop α))

instance WithBot.addCommMonoidWithOne {α : Type u} [AddCommMonoidWithOne α] : AddCommMonoidWithOne (WithBot α)

Equations

• WithBot.addCommMonoidWithOne = WithTop.addCommMonoidWithOne

instance WithBot.zeroLEOneClass {α : Type u} [Zero α] [One α] [LE α] [ZeroLEOneClass α] : ZeroLEOneClass (WithBot α)

Equations

• @WithBot.zeroLEOneClass = @WithBot.zeroLEOneClass.proof_1

theorem WithBot.coe_zero {α : Type u} [Zero α] : ↑0 = 0

theorem WithBot.coe_one {α : Type u} [One α] : ↑1 = 1

theorem WithBot.coe_eq_zero {α : Type u} [Zero α] {a : α} : ↑a = 0 ↔ a = 0

theorem WithBot.coe_eq_one {α : Type u} [One α] {a : α} : ↑a = 1 ↔ a = 1

@[simp]

theorem WithBot.unbot_zero {α : Type u} [Zero α] : WithBot.unbot 0 (_ : ↑0 ≠ ⊥) = 0

@[simp]

theorem WithBot.unbot_one {α : Type u} [One α] : WithBot.unbot 1 (_ : ↑1 ≠ ⊥) = 1

@[simp]

theorem WithBot.unbot_zero' {α : Type u} [Zero α] (d : α) : WithBot.unbot' d 0 = 0

@[simp]

theorem WithBot.unbot_one' {α : Type u} [One α] (d : α) : WithBot.unbot' d 1 = 1

@[simp]

theorem WithBot.coe_nonneg {α : Type u} [Zero α] [LE α] {a : α} : 0 ≤ ↑a ↔ 0 ≤ a

@[simp]

theorem WithBot.one_le_coe {α : Type u} [One α] [LE α] {a : α} : 1 ≤ ↑a ↔ 1 ≤ a

@[simp]

theorem WithBot.coe_le_zero {α : Type u} [Zero α] [LE α] {a : α} : ↑a ≤ 0 ↔ a ≤ 0

@[simp]

theorem WithBot.coe_le_one {α : Type u} [One α] [LE α] {a : α} : ↑a ≤ 1 ↔ a ≤ 1

@[simp]

theorem WithBot.coe_pos {α : Type u} [Zero α] [LT α] {a : α} : 0 < ↑a ↔ 0 < a

@[simp]

theorem WithBot.one_lt_coe {α : Type u} [One α] [LT α] {a : α} : 1 < ↑a ↔ 1 < a

@[simp]

theorem WithBot.coe_lt_zero {α : Type u} [Zero α] [LT α] {a : α} : ↑a < 0 ↔ a < 0

@[simp]

theorem WithBot.coe_lt_one {α : Type u} [One α] [LT α] {a : α} : ↑a < 1 ↔ a < 1

@[simp]

theorem WithBot.map_zero {α : Type u} {β : Type u_1} [Zero α] (f : α → β) : WithBot.map f 0 = ↑(f 0)

@[simp]

theorem WithBot.map_one {α : Type u} {β : Type u_1} [One α] (f : α → β) : WithBot.map f 1 = ↑(f 1)

theorem WithBot.coe_nat {α : Type u} [AddMonoidWithOne α] (n : ℕ) : ↑↑n = ↑n

@[simp]

theorem WithBot.nat_ne_bot {α : Type u} [AddMonoidWithOne α] (n : ℕ) : ↑n ≠ ⊥

@[simp]

theorem WithBot.bot_ne_nat {α : Type u} [AddMonoidWithOne α] (n : ℕ) : ⊥ ≠ ↑n

theorem WithBot.coe_add {α : Type u} [Add α] (a : α) (b : α) : ↑(a + b) = ↑a + ↑b

@[deprecated]

theorem WithBot.coe_bit0 {α : Type u} [Add α] {x : α} : ↑(bit0 x) = bit0 ↑x

@[deprecated]

theorem WithBot.coe_bit1 {α : Type u} [Add α] [One α] {a : α} : ↑(bit1 a) = bit1 ↑a

@[simp]

theorem WithBot.bot_add {α : Type u} [Add α] (a : WithBot α) : ⊥ + a = ⊥

@[simp]

theorem WithBot.add_bot {α : Type u} [Add α] (a : WithBot α) : a + ⊥ = ⊥

@[simp]

theorem WithBot.add_eq_bot {α : Type u} [Add α] {a : WithBot α} {b : WithBot α} : a + b = ⊥ ↔ a = ⊥ ∨ b = ⊥

theorem WithBot.add_ne_bot {α : Type u} [Add α] {a : WithBot α} {b : WithBot α} : a + b ≠ ⊥ ↔ a ≠ ⊥ ∧ b ≠ ⊥

theorem WithBot.bot_lt_add {α : Type u} [Add α] [LT α] {a : WithBot α} {b : WithBot α} : ⊥ < a + b ↔ ⊥ < a ∧ ⊥ < b

theorem WithBot.add_eq_coe {α : Type u} [Add α] {a : WithBot α} {b : WithBot α} {x : α} : a + b = ↑x ↔ ∃ a' b', ↑a' = a ∧ ↑b' = b ∧ a' + b' = x

theorem WithBot.add_coe_eq_bot_iff {α : Type u} [Add α] {a : WithBot α} {y : α} : a + ↑y = ⊥ ↔ a = ⊥

theorem WithBot.coe_add_eq_bot_iff {α : Type u} [Add α] {b : WithBot α} {x : α} : ↑x + b = ⊥ ↔ b = ⊥

theorem WithBot.add_right_cancel_iff {α : Type u} [Add α] {a : WithBot α} {b : WithBot α} {c : WithBot α} [IsRightCancelAdd α] (ha : a ≠ ⊥) : b + a = c + a ↔ b = c

theorem WithBot.add_right_cancel {α : Type u} [Add α] {a : WithBot α} {b : WithBot α} {c : WithBot α} [IsRightCancelAdd α] (ha : a ≠ ⊥) (h : b + a = c + a) : b = c

theorem WithBot.add_left_cancel_iff {α : Type u} [Add α] {a : WithBot α} {b : WithBot α} {c : WithBot α} [IsLeftCancelAdd α] (ha : a ≠ ⊥) : a + b = a + c ↔ b = c

theorem WithBot.add_left_cancel {α : Type u} [Add α] {a : WithBot α} {b : WithBot α} {c : WithBot α} [IsLeftCancelAdd α] (ha : a ≠ ⊥) (h : a + b = a + c) : b = c

@[simp]

theorem WithBot.map_add {α : Type u} {β : Type v} [Add α] {F : Type u_1} [Add β] [AddHomClass F α β] (f : F) (a : WithBot α) (b : WithBot α) : WithBot.map (↑f) (a + b) = WithBot.map (↑f) a + WithBot.map (↑f) b

theorem ZeroHom.withBotMap.proof_1 {M : Type u_2} {N : Type u_1} [Zero M] [Zero N] (f : ZeroHom M N) : WithBot.map (↑f) 0 = 0

def ZeroHom.withBotMap {M : Type u_1} {N : Type u_2} [Zero M] [Zero N] (f : ZeroHom M N) : ZeroHom (WithBot M) (WithBot N)

A version of WithBot.map for ZeroHoms

Equations

• ZeroHom.withBotMap f = { toFun := WithBot.map ↑f, map_zero' := (_ : WithBot.map (↑f) 0 = 0) }

@[simp]

theorem OneHom.withBotMap_apply {M : Type u_1} {N : Type u_2} [One M] [One N] (f : OneHom M N) : ↑(OneHom.withBotMap f) = WithBot.map ↑f

@[simp]

theorem ZeroHom.withBotMap_apply {M : Type u_1} {N : Type u_2} [Zero M] [Zero N] (f : ZeroHom M N) : ↑(ZeroHom.withBotMap f) = WithBot.map ↑f

def OneHom.withBotMap {M : Type u_1} {N : Type u_2} [One M] [One N] (f : OneHom M N) : OneHom (WithBot M) (WithBot N)

A version of WithBot.map for OneHoms.

Equations

• OneHom.withBotMap f = { toFun := WithBot.map ↑f, map_one' := (_ : WithBot.map (↑f) 1 = 1) }

@[simp]

theorem AddHom.withBotMap_apply {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) : ↑(AddHom.withBotMap f) = WithBot.map ↑f

def AddHom.withBotMap {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) : AddHom (WithBot M) (WithBot N)

A version of WithBot.map for AddHoms.

Equations

• AddHom.withBotMap f = { toFun := WithBot.map ↑f, map_add' := (_ : ∀ (a b : WithBot M), WithBot.map (↑f) (a + b) = WithBot.map (↑f) a + WithBot.map (↑f) b) }

@[simp]

theorem AddMonoidHom.withBotMap_apply {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) : ↑(AddMonoidHom.withBotMap f) = WithBot.map ↑f

def AddMonoidHom.withBotMap {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) : WithBot M →+ WithBot N

A version of WithBot.map for AddMonoidHoms.

Equations

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

instance WithBot.covariantClass_add_le {α : Type u} [Add α] [Preorder α] [CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] : CovariantClass (WithBot α) (WithBot α) (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

Equations

• @WithBot.covariantClass_add_le = @WithBot.covariantClass_add_le.proof_1

instance WithBot.covariantClass_swap_add_le {α : Type u} [Add α] [Preorder α] [CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] : CovariantClass (WithBot α) (WithBot α) (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

Equations

• @WithBot.covariantClass_swap_add_le = @WithBot.covariantClass_swap_add_le.proof_1

instance WithBot.contravariantClass_add_lt {α : Type u} [Add α] [Preorder α] [ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] : ContravariantClass (WithBot α) (WithBot α) (fun x x_1 => x + x_1) fun x x_1 => x < x_1

Equations

• @WithBot.contravariantClass_add_lt = @WithBot.contravariantClass_add_lt.proof_1

instance WithBot.contravariantClass_swap_add_lt {α : Type u} [Add α] [Preorder α] [ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] : ContravariantClass (WithBot α) (WithBot α) (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1

Equations

• @WithBot.contravariantClass_swap_add_lt = @WithBot.contravariantClass_swap_add_lt.proof_1

theorem WithBot.le_of_add_le_add_left {α : Type u} [Add α] {a : WithBot α} {b : WithBot α} {c : WithBot α} [Preorder α] [ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (ha : a ≠ ⊥) (h : a + b ≤ a + c) : b ≤ c

theorem WithBot.le_of_add_le_add_right {α : Type u} [Add α] {a : WithBot α} {b : WithBot α} {c : WithBot α} [Preorder α] [ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (ha : a ≠ ⊥) (h : b + a ≤ c + a) : b ≤ c

theorem WithBot.add_lt_add_left {α : Type u} [Add α] {a : WithBot α} {b : WithBot α} {c : WithBot α} [Preorder α] [CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] (ha : a ≠ ⊥) (h : b < c) : a + b < a + c

theorem WithBot.add_lt_add_right {α : Type u} [Add α] {a : WithBot α} {b : WithBot α} {c : WithBot α} [Preorder α] [CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] (ha : a ≠ ⊥) (h : b < c) : b + a < c + a

theorem WithBot.add_le_add_iff_left {α : Type u} [Add α] {a : WithBot α} {b : WithBot α} {c : WithBot α} [Preorder α] [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] (ha : a ≠ ⊥) : a + b ≤ a + c ↔ b ≤ c

theorem WithBot.add_le_add_iff_right {α : Type u} [Add α] {a : WithBot α} {b : WithBot α} {c : WithBot α} [Preorder α] [CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (ha : a ≠ ⊥) : b + a ≤ c + a ↔ b ≤ c

theorem WithBot.add_lt_add_iff_left {α : Type u} [Add α] {a : WithBot α} {b : WithBot α} {c : WithBot α} [Preorder α] [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] (ha : a ≠ ⊥) : a + b < a + c ↔ b < c

theorem WithBot.add_lt_add_iff_right {α : Type u} [Add α] {a : WithBot α} {b : WithBot α} {c : WithBot α} [Preorder α] [CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] [ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] (ha : a ≠ ⊥) : b + a < c + a ↔ b < c

theorem WithBot.add_lt_add_of_le_of_lt {α : Type u} [Add α] {a : WithBot α} {b : WithBot α} {c : WithBot α} {d : WithBot α} [Preorder α] [CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (hb : b ≠ ⊥) (hab : a ≤ b) (hcd : c < d) : a + c < b + d

theorem WithBot.add_lt_add_of_lt_of_le {α : Type u} [Add α] {a : WithBot α} {b : WithBot α} {c : WithBot α} {d : WithBot α} [Preorder α] [CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] (hd : d ≠ ⊥) (hab : a < b) (hcd : c ≤ d) : a + c < b + d

instance WithBot.orderedAddCommMonoid {α : Type u} [OrderedAddCommMonoid α] : OrderedAddCommMonoid (WithBot α)

Equations

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

instance WithBot.linearOrderedAddCommMonoid {α : Type u} [LinearOrderedAddCommMonoid α] : LinearOrderedAddCommMonoid (WithBot α)

Equations

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