Adjoining top/bottom elements to ordered monoids.

ink

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

Equations

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

ink

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

Equations

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

Equations

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

ink

@[simp]

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

ink

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

Equations

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

Equations

• WithTop.zeroLEOneClass = { zero_le_one := (_ : some 0 ≤ some 1) }

ink

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

Equations

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

ink

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

ink

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

instance WithTop.covariantClass_add_le {α : Type u} [inst : Add α] [inst : LE α] [inst : 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

ink

instance WithTop.covariantClass_swap_add_le {α : Type u} [inst : Add α] [inst : LE α] [inst : 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

ink

instance WithTop.contravariantClass_add_lt {α : Type u} [inst : Add α] [inst : LT α] [inst : 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

ink

instance WithTop.contravariantClass_swap_add_lt {α : Type u} [inst : Add α] [inst : LT α] [inst : 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

ink

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

ink

theorem WithTop.le_of_add_le_add_right {α : Type u} [inst : Add α] {a : WithTop α} {b : WithTop α} {c : WithTop α} [inst : LE α] [inst : 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

ink

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

ink

theorem WithTop.add_lt_add_right {α : Type u} [inst : Add α] {a : WithTop α} {b : WithTop α} {c : WithTop α} [inst : LT α] [inst : 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

ink

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

ink

theorem WithTop.add_le_add_iff_right {α : Type u} [inst : Add α] {a : WithTop α} {b : WithTop α} {c : WithTop α} [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst : 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

ink

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

ink

theorem WithTop.add_lt_add_iff_right {α : Type u} [inst : Add α] {a : WithTop α} {b : WithTop α} {c : WithTop α} [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : 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

ink

theorem WithTop.add_lt_add_of_le_of_lt {α : Type u} [inst : Add α] {a : WithTop α} {b : WithTop α} {c : WithTop α} {d : WithTop α} [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : 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

ink

theorem WithTop.add_lt_add_of_lt_of_le {α : Type u} [inst : Add α] {a : WithTop α} {b : WithTop α} {c : WithTop α} {d : WithTop α} [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst : 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

ink

@[simp]

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

ink

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

Equations

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

ink

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

Equations

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

ink

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

Equations

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

ink

instance WithTop.addMonoid {α : Type u} [inst : 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

ink

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

Equations

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

ink

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

Equations

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

ink

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

Equations

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

ink

instance WithTop.orderedAddCommMonoid {α : Type u} [inst : 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)

ink

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

Equations

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

ink

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

Equations

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

ink

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

Equations

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

ink

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

Equations

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

Coercion from α to WithTop α as an AddMonoidHom.

Equations

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

ink

@[simp]

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

ink

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

ink

def ZeroHom.withTopMap {M : Type u_1} {N : Type u_2} [inst : Zero M] [inst : 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) }

ink

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

Equations

• (_ : WithTop.map (↑f) 0 = 0) = (_ : WithTop.map (↑f) 0 = 0)

ink

@[simp]

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

ink

@[simp]

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

ink

def OneHom.withTopMap {M : Type u_1} {N : Type u_2} [inst : One M] [inst : 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) }

ink

@[simp]

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

ink

def AddHom.withTopMap {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : 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) }

ink

@[simp]

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

ink

def AddMonoidHom.withTopMap {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : 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.

ink

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

Equations

• WithBot.zero = WithTop.zero

ink

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

Equations

• WithBot.one = WithTop.one

ink

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

Equations

• WithBot.add = WithTop.add

ink

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

Equations

• WithBot.AddSemigroup = WithTop.addSemigroup

ink

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

Equations

• WithBot.addCommSemigroup = WithTop.addCommSemigroup

ink

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

Equations

• WithBot.addZeroClass = WithTop.addZeroClass

ink

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

Equations

• WithBot.addMonoid = WithTop.addMonoid

ink

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

Equations

• WithBot.addCommMonoid = WithTop.addCommMonoid

ink

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

Equations

• WithBot.addMonoidWithOne = WithTop.addMonoidWithOne

ink

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

Equations

• WithBot.addCommMonoidWithOne = WithTop.addCommMonoidWithOne

ink

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

Equations

• WithBot.zeroLEOneClass = { zero_le_one := (_ : some 0 ≤ some 1) }

ink

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

ink

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

ink

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

@[simp]

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

ink

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

Equations

• (_ : WithBot.map (↑f) 0 = 0) = (_ : WithBot.map (↑f) 0 = 0)

ink

def ZeroHom.withBotMap {M : Type u_1} {N : Type u_2} [inst : Zero M] [inst : 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) }

ink

@[simp]

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

ink

@[simp]

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

ink

def OneHom.withBotMap {M : Type u_1} {N : Type u_2} [inst : One M] [inst : 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) }

ink

@[simp]

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

ink

def AddHom.withBotMap {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : 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) }

ink

@[simp]

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

ink

def AddMonoidHom.withBotMap {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : 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.

ink

instance WithBot.covariantClass_add_le {α : Type u} [inst : Add α] [inst : Preorder α] [inst : 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

ink

instance WithBot.covariantClass_swap_add_le {α : Type u} [inst : Add α] [inst : Preorder α] [inst : 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

ink

instance WithBot.contravariantClass_add_lt {α : Type u} [inst : Add α] [inst : Preorder α] [inst : 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

ink

instance WithBot.contravariantClass_swap_add_lt {α : Type u} [inst : Add α] [inst : Preorder α] [inst : 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

ink

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

ink

theorem WithBot.le_of_add_le_add_right {α : Type u} [inst : Add α] {a : WithBot α} {b : WithBot α} {c : WithBot α} [inst : Preorder α] [inst : 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

ink

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

ink

theorem WithBot.add_lt_add_right {α : Type u} [inst : Add α] {a : WithBot α} {b : WithBot α} {c : WithBot α} [inst : Preorder α] [inst : 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

ink

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

ink

theorem WithBot.add_le_add_iff_right {α : Type u} [inst : Add α] {a : WithBot α} {b : WithBot α} {c : WithBot α} [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst : 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

ink

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

ink

theorem WithBot.add_lt_add_iff_right {α : Type u} [inst : Add α] {a : WithBot α} {b : WithBot α} {c : WithBot α} [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : 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

ink

theorem WithBot.add_lt_add_of_le_of_lt {α : Type u} [inst : Add α] {a : WithBot α} {b : WithBot α} {c : WithBot α} {d : WithBot α} [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : 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

ink

theorem WithBot.add_lt_add_of_lt_of_le {α : Type u} [inst : Add α] {a : WithBot α} {b : WithBot α} {c : WithBot α} {d : WithBot α} [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst : 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

ink

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

Equations

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

ink

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

Equations

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