Documentation

Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Adjoining top/bottom elements to ordered monoids. #

source
@[instance_reducible]
instance WithTop.one {α : Type u} [One α] :
One (WithTop α)
source
@[instance_reducible]
instance WithTop.zero {α : Type u} [Zero α] :
Zero (WithTop α)
source
@[simp]
theorem WithTop.coe_one {α : Type u} [One α] :
↑1 = 1
source
@[simp]
theorem WithTop.coe_zero {α : Type u} [Zero α] :
↑0 = 0
source
@[simp]
theorem WithTop.coe_eq_one {α : Type u} [One α] {a : α} :
↑a = 1 ↔ a = 1
source
@[simp]
theorem WithTop.coe_eq_zero {α : Type u} [Zero α] {a : α} :
↑a = 0 ↔ a = 0
source
theorem WithTop.coe_ne_one {α : Type u} [One α] {a : α} :
↑a ≠ 1 ↔ a ≠ 1
source
theorem WithTop.coe_ne_zero {α : Type u} [Zero α] {a : α} :
↑a ≠ 0 ↔ a ≠ 0
source
@[simp]
theorem WithTop.one_eq_coe {α : Type u} [One α] {a : α} :
1 = ↑a ↔ a = 1
source
@[simp]
theorem WithTop.zero_eq_coe {α : Type u} [Zero α] {a : α} :
0 = ↑a ↔ a = 0
source
@[simp]
theorem WithTop.top_ne_one {α : Type u} [One α] :
⊤ ≠ 1
source
@[simp]
theorem WithTop.top_ne_zero {α : Type u} [Zero α] :
⊤ ≠ 0
source
@[simp]
theorem WithTop.one_ne_top {α : Type u} [One α] :
1 ≠ ⊤
source
@[simp]
theorem WithTop.zero_ne_top {α : Type u} [Zero α] :
0 ≠ ⊤
source
@[simp]
theorem WithTop.untop_one {α : Type u} [One α] :
untop 1 ⋯ = 1
source
@[simp]
theorem WithTop.untop_zero {α : Type u} [Zero α] :
untop 0 ⋯ = 0
source
@[simp]
theorem WithTop.untopD_one {α : Type u} [One α] (d : α) :
untopD d 1 = 1
source
@[simp]
theorem WithTop.untopD_zero {α : Type u} [Zero α] (d : α) :
untopD d 0 = 0
source
@[simp]
theorem WithTop.one_le_coe {α : Type u} [One α] [LE α] {a : α} :
1 ≤ ↑a ↔ 1 ≤ a
source
@[simp]
theorem WithTop.coe_nonneg {α : Type u} [Zero α] [LE α] {a : α} :
0 ≤ ↑a ↔ 0 ≤ a
source
@[simp]
theorem WithTop.coe_le_one {α : Type u} [One α] [LE α] {a : α} :
↑a ≤ 1 ↔ a ≤ 1
source
@[simp]
theorem WithTop.coe_le_zero {α : Type u} [Zero α] [LE α] {a : α} :
↑a ≤ 0 ↔ a ≤ 0
source
@[simp]
theorem WithTop.one_lt_coe {α : Type u} [One α] [LT α] {a : α} :
1 < ↑a ↔ 1 < a
source
@[simp]
theorem WithTop.coe_pos {α : Type u} [Zero α] [LT α] {a : α} :
0 < ↑a ↔ 0 < a
source
@[simp]
theorem WithTop.coe_lt_one {α : Type u} [One α] [LT α] {a : α} :
↑a < 1 ↔ a < 1
source
@[simp]
theorem WithTop.coe_lt_zero {α : Type u} [Zero α] [LT α] {a : α} :
↑a < 0 ↔ a < 0
source
@[simp]
theorem WithTop.map_one {α : Type u} [One α] {β : Type u_1} (f : α → β) :
map f 1 = ↑(f 1)
source
@[simp]
theorem WithTop.map_zero {α : Type u} [Zero α] {β : Type u_1} (f : α → β) :
map f 0 = ↑(f 0)
source
theorem WithTop.map_eq_one_iff {β : Type v} {α : Type u_1} {f : α → β} {v : WithTop α} [One β] :
map f v = 1 ↔ ∃ (x : α), v = ↑x ∧ f x = 1
source
theorem WithTop.map_eq_zero_iff {β : Type v} {α : Type u_1} {f : α → β} {v : WithTop α} [Zero β] :
map f v = 0 ↔ ∃ (x : α), v = ↑x ∧ f x = 0
source
theorem WithTop.one_eq_map_iff {β : Type v} {α : Type u_1} {f : α → β} {v : WithTop α} [One β] :
1 = map f v ↔ ∃ (x : α), v = ↑x ∧ f x = 1
source
theorem WithTop.zero_eq_map_iff {β : Type v} {α : Type u_1} {f : α → β} {v : WithTop α} [Zero β] :
0 = map f v ↔ ∃ (x : α), v = ↑x ∧ f x = 0
source
instance WithTop.zeroLEOneClass {α : Type u} [One α] [Zero α] [LE α] [ZeroLEOneClass α] :
ZeroLEOneClass (WithTop α)
source
instance WithTop.instIsBotOneClass {α : Type u} [One α] [LE α] [IsBotOneClass α] :
IsBotOneClass (WithTop α)
source
instance WithTop.instIsBotZeroClass {α : Type u} [Zero α] [LE α] [IsBotZeroClass α] :
IsBotZeroClass (WithTop α)
source
@[instance_reducible]
instance WithTop.add {α : Type u} [Add α] :
Add (WithTop α)
source
@[simp]
theorem WithTop.coe_add {α : Type u} [Add α] (a b : α) :
↑(a + b) = ↑a + ↑b
source
@[simp]
theorem WithTop.top_add {α : Type u} [Add α] (x : WithTop α) :
⊤ + x = ⊤
source
@[simp]
theorem WithTop.add_top {α : Type u} [Add α] (x : WithTop α) :
x + ⊤ = ⊤
source
@[simp]
theorem WithTop.add_eq_top {α : Type u} [Add α] {x y : WithTop α} :
x + y = ⊤ ↔ x = ⊤ ∨ y = ⊤
source
theorem WithTop.add_ne_top {α : Type u} [Add α] {x y : WithTop α} :
x + y ≠ ⊤ ↔ x ≠ ⊤ ∧ y ≠ ⊤
source
@[simp]
theorem WithTop.add_lt_top {α : Type u} [Add α] {x y : WithTop α} [LT α] :
x + y < ⊤ ↔ x < ⊤ ∧ y < ⊤
source
theorem WithTop.add_eq_coe {α : Type u} [Add α] {a b : WithTop α} {c : α} :
a + b = ↑c ↔ ∃ (a' : α), ∃ (b' : α), ↑a' = a ∧ ↑b' = b ∧ a' + b' = c
source
theorem WithTop.add_coe_eq_top_iff {α : Type u} [Add α] {x : WithTop α} {b : α} :
x + ↑b = ⊤ ↔ x = ⊤
source
theorem WithTop.coe_add_eq_top_iff {α : Type u} [Add α] {y : WithTop α} {a : α} :
↑a + y = ⊤ ↔ y = ⊤
source
theorem IsAddLeftRegular.withTop {α : Type u} [Add α] {a : α} (ha : IsAddLeftRegular a) :
IsAddLeftRegular ↑a
source
theorem IsAddRightRegular.withTop {α : Type u} [Add α] {a : α} (ha : IsAddRightRegular a) :
IsAddRightRegular ↑a
source
theorem AddLECancellable.withTop {α : Type u} [Add α] {a : α} [LE α] (ha : AddLECancellable a) :
AddLECancellable ↑a
source
theorem WithTop.add_right_inj {α : Type u} [Add α] {x y z : WithTop α} [IsRightCancelAdd α] (hz : z ≠ ⊤) :
x + z = y + z ↔ x = y
source
theorem WithTop.add_right_cancel {α : Type u} [Add α] {x y z : WithTop α} [IsRightCancelAdd α] (hz : z ≠ ⊤) (h : x + z = y + z) :
x = y
source
theorem WithTop.add_left_inj {α : Type u} [Add α] {x y z : WithTop α} [IsLeftCancelAdd α] (hx : x ≠ ⊤) :
x + y = x + z ↔ y = z
source
theorem WithTop.add_left_cancel {α : Type u} [Add α] {x y z : WithTop α} [IsLeftCancelAdd α] (hx : x ≠ ⊤) (h : x + y = x + z) :
y = z
source
instance WithTop.addLeftMono {α : Type u} [Add α] [LE α] [AddLeftMono α] :
AddLeftMono (WithTop α)
source
instance WithTop.addRightMono {α : Type u} [Add α] [LE α] [AddRightMono α] :
AddRightMono (WithTop α)
source
instance WithTop.addLeftReflectLT {α : Type u} [Add α] [LT α] [AddLeftReflectLT α] :
AddLeftReflectLT (WithTop α)
source
instance WithTop.addRightReflectLT {α : Type u} [Add α] [LT α] [AddRightReflectLT α] :
AddRightReflectLT (WithTop α)
source
theorem WithTop.le_of_add_le_add_left {α : Type u} [Add α] {x y z : WithTop α} [LE α] [AddLeftReflectLE α] (hx : x ≠ ⊤) :
x + y ≤ x + z → y ≤ z
source
theorem WithTop.le_of_add_le_add_right {α : Type u} [Add α] {x y z : WithTop α} [LE α] [AddRightReflectLE α] (hz : z ≠ ⊤) :
x + z ≤ y + z → x ≤ y
source
theorem WithTop.add_lt_add_left {α : Type u} [Add α] {x y z : WithTop α} [LT α] [AddLeftStrictMono α] (hx : x ≠ ⊤) :
y < z → x + y < x + z
source
theorem WithTop.add_lt_add_right {α : Type u} [Add α] {x y z : WithTop α} [LT α] [AddRightStrictMono α] (hz : z ≠ ⊤) :
x < y → x + z < y + z
source
theorem WithTop.add_lt_add {α : Type u} [Add α] {w x y z : WithTop α} [Preorder α] [AddLeftStrictMono α] [AddRightStrictMono α] (xz : x < z) (yw : y < w) :
x + y < z + w
source
theorem WithTop.add_le_add_iff_left {α : Type u} [Add α] {x y z : WithTop α} [LE α] [AddLeftMono α] [AddLeftReflectLE α] (hx : x ≠ ⊤) :
x + y ≤ x + z ↔ y ≤ z
source
theorem WithTop.add_le_add_iff_right {α : Type u} [Add α] {x y z : WithTop α} [LE α] [AddRightMono α] [AddRightReflectLE α] (hz : z ≠ ⊤) :
x + z ≤ y + z ↔ x ≤ y
source
theorem WithTop.add_lt_add_iff_left {α : Type u} [Add α] {x y z : WithTop α} [LT α] [AddLeftStrictMono α] [AddLeftReflectLT α] (hx : x ≠ ⊤) :
x + y < x + z ↔ y < z
source
theorem WithTop.add_lt_add_iff_right {α : Type u} [Add α] {x y z : WithTop α} [LT α] [AddRightStrictMono α] [AddRightReflectLT α] (hz : z ≠ ⊤) :
x + z < y + z ↔ x < y
source
theorem WithTop.add_lt_add_of_le_of_lt {α : Type u} [Add α] {w x y z : WithTop α} [Preorder α] [AddLeftStrictMono α] [AddRightMono α] (hw : w ≠ ⊤) (hwy : w ≤ y) (hxz : x < z) :
w + x < y + z
source
theorem WithTop.add_lt_add_of_lt_of_le {α : Type u} [Add α] {w x y z : WithTop α} [Preorder α] [AddLeftMono α] [AddRightStrictMono α] (hx : x ≠ ⊤) (hwy : w < y) (hxz : x ≤ z) :
w + x < y + z
source
theorem WithTop.addLECancellable_of_ne_top {α : Type u} [Add α] {x : WithTop α} [LE α] [AddLeftReflectLE α] (hx : x ≠ ⊤) :
AddLECancellable x
source
theorem WithTop.addLECancellable_of_lt_top {α : Type u} [Add α] {x : WithTop α} [Preorder α] [AddLeftReflectLE α] (hx : x < ⊤) :
AddLECancellable x
source
theorem WithTop.addLECancellable_coe {α : Type u} [Add α] [LE α] [AddLeftReflectLE α] (a : α) :
AddLECancellable ↑a
source
theorem WithTop.addLECancellable_iff_ne_top {α : Type u} [Add α] {x : WithTop α} [Nonempty α] [Preorder α] [AddLeftReflectLE α] :
AddLECancellable x ↔ x ≠ ⊤
source
@[simp]
theorem WithTop.map_add {α : Type u} {β : Type v} [Add α] {F : Type u_1} [Add β] [FunLike F α β] [AddHomClass F α β] (f : F) (a b : WithTop α) :
map (⇑f) (a + b) = map (⇑f) a + map (⇑f) b
source
@[instance_reducible]
instance WithTop.addSemigroup {α : Type u} [AddSemigroup α] :
AddSemigroup (WithTop α)
source
@[instance_reducible]
instance WithTop.addCommSemigroup {α : Type u} [AddCommSemigroup α] :
AddCommSemigroup (WithTop α)
source
@[instance_reducible]
instance WithTop.addZeroClass {α : Type u} [AddZeroClass α] :
AddZeroClass (WithTop α)
source
@[instance_reducible]
instance WithTop.addMonoid {α : Type u} [AddMonoid α] :
AddMonoid (WithTop α)
source
@[simp]
theorem WithTop.coe_nsmul {α : Type u} [AddMonoid α] (a : α) (n : ℕ) :
↑(n • a) = n • ↑a
source
def WithTop.addHom {α : Type u} [AddMonoid α] :
α →+ WithTop α

Coercion from α to WithTop α as an AddMonoidHom.

Instances For
    source
    @[simp]
    theorem WithTop.coe_addHom {α : Type u} [AddMonoid α] :
    ⇑addHom = some
    source
    @[instance_reducible]
    instance WithTop.addCommMonoid {α : Type u} [AddCommMonoid α] :
    AddCommMonoid (WithTop α)
    source
    @[instance_reducible]
    instance WithTop.natCast {α : Type u} [NatCast α] :
    NatCast (WithTop α)
    source
    @[instance_reducible]
    instance WithTop.addMonoidWithOne {α : Type u} [AddMonoidWithOne α] :
    AddMonoidWithOne (WithTop α)
    source
    @[simp]
    theorem WithTop.coe_natCast {α : Type u} [AddMonoidWithOne α] (n : ℕ) :
    ↑↑n = ↑n
    source
    @[simp]
    theorem WithTop.top_ne_natCast {α : Type u} [AddMonoidWithOne α] (n : ℕ) :
    ⊤ ≠ ↑n
    source
    @[simp]
    theorem WithTop.natCast_ne_top {α : Type u} [AddMonoidWithOne α] (n : ℕ) :
    ↑n ≠ ⊤
    source
    @[simp]
    theorem WithTop.natCast_lt_top {α : Type u} [AddMonoidWithOne α] [LT α] (n : ℕ) :
    ↑n < ⊤
    source
    @[simp]
    theorem WithTop.coe_ofNat {α : Type u} [AddMonoidWithOne α] (n : ℕ) [n.AtLeastTwo] :
    ↑(OfNat.ofNat n) = OfNat.ofNat n
    source
    @[simp]
    theorem WithTop.coe_eq_ofNat {α : Type u} [AddMonoidWithOne α] (n : ℕ) [n.AtLeastTwo] (m : α) :
    ↑m = OfNat.ofNat n ↔ m = OfNat.ofNat n
    source
    @[simp]
    theorem WithTop.ofNat_eq_coe {α : Type u} [AddMonoidWithOne α] (n : ℕ) [n.AtLeastTwo] (m : α) :
    OfNat.ofNat n = ↑m ↔ OfNat.ofNat n = m
    source
    @[simp]
    theorem WithTop.ofNat_ne_top {α : Type u} [AddMonoidWithOne α] (n : ℕ) [n.AtLeastTwo] :
    OfNat.ofNat n ≠ ⊤
    source
    @[simp]
    theorem WithTop.top_ne_ofNat {α : Type u} [AddMonoidWithOne α] (n : ℕ) [n.AtLeastTwo] :
    ⊤ ≠ OfNat.ofNat n
    source
    @[simp]
    theorem WithTop.map_ofNat {α : Type u} {β : Type v} [AddMonoidWithOne α] {f : α → β} (n : ℕ) [n.AtLeastTwo] :
    map f (OfNat.ofNat n) = ↑(f (OfNat.ofNat n))
    source
    @[simp]
    theorem WithTop.map_natCast {α : Type u} {β : Type v} [AddMonoidWithOne α] {f : α → β} (n : ℕ) :
    map f ↑n = ↑(f ↑n)
    source
    theorem WithTop.map_eq_ofNat_iff {α : Type u} {β : Type v} [AddMonoidWithOne α] {f : β → α} {n : ℕ} [n.AtLeastTwo] {a : WithTop β} :
    map f a = OfNat.ofNat n ↔ ∃ (x : β), a = ↑x ∧ f x = ↑n
    source
    theorem WithTop.ofNat_eq_map_iff {α : Type u} {β : Type v} [AddMonoidWithOne α] {f : β → α} {n : ℕ} [n.AtLeastTwo] {a : WithTop β} :
    OfNat.ofNat n = map f a ↔ ∃ (x : β), a = ↑x ∧ f x = ↑n
    source
    theorem WithTop.map_eq_natCast_iff {α : Type u} {β : Type v} [AddMonoidWithOne α] {f : β → α} {n : ℕ} {a : WithTop β} :
    map f a = ↑n ↔ ∃ (x : β), a = ↑x ∧ f x = ↑n
    source
    theorem WithTop.natCast_eq_map_iff {α : Type u} {β : Type v} [AddMonoidWithOne α] {f : β → α} {n : ℕ} {a : WithTop β} :
    ↑n = map f a ↔ ∃ (x : β), a = ↑x ∧ f x = ↑n
    source
    instance WithTop.charZero {α : Type u} [AddMonoidWithOne α] [CharZero α] :
    CharZero (WithTop α)
    source
    @[instance_reducible]
    instance WithTop.addCommMonoidWithOne {α : Type u} [AddCommMonoidWithOne α] :
    AddCommMonoidWithOne (WithTop α)
    source
    instance WithTop.existsAddOfLE {α : Type u} [LE α] [Add α] [ExistsAddOfLE α] :
    ExistsAddOfLE (WithTop α)
    source
    @[simp]
    theorem WithTop.one_lt_top {α : Type u} [One α] [LT α] :
    1 < ⊤
    source
    @[simp]
    theorem WithTop.top_pos {α : Type u} [Zero α] [LT α] :
    0 < ⊤
    source
    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.

    Instances For
      source
      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

      Instances For
        source
        @[simp]
        theorem ZeroHom.withTopMap_apply {M : Type u_1} {N : Type u_2} [Zero M] [Zero N] (f : ZeroHom M N) :
        ⇑f.withTopMap = WithTop.map ⇑f
        source
        @[simp]
        theorem OneHom.withTopMap_apply {M : Type u_1} {N : Type u_2} [One M] [One N] (f : OneHom M N) :
        ⇑f.withTopMap = WithTop.map ⇑f
        source
        def AddHom.withTopMap {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : M →ₙ+ N) :
        WithTop M →ₙ+ WithTop N

        A version of WithTop.map for AddHoms.

        Instances For
          source
          @[simp]
          theorem AddHom.withTopMap_apply {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : M →ₙ+ N) :
          ⇑f.withTopMap = WithTop.map ⇑f
          source
          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.

          Instances For
            source
            @[simp]
            theorem AddMonoidHom.withTopMap_apply {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) :
            ⇑f.withTopMap = WithTop.map ⇑f
            source
            @[instance_reducible]
            instance WithBot.one {α : Type u} [One α] :
            One (WithBot α)
            source
            @[instance_reducible]
            instance WithBot.zero {α : Type u} [Zero α] :
            Zero (WithBot α)
            source
            @[simp]
            theorem WithBot.coe_one {α : Type u} [One α] :
            ↑1 = 1
            source
            @[simp]
            theorem WithBot.coe_zero {α : Type u} [Zero α] :
            ↑0 = 0
            source
            @[simp]
            theorem WithBot.coe_eq_one {α : Type u} [One α] {a : α} :
            ↑a = 1 ↔ a = 1
            source
            @[simp]
            theorem WithBot.coe_eq_zero {α : Type u} [Zero α] {a : α} :
            ↑a = 0 ↔ a = 0
            source
            @[simp]
            theorem WithBot.one_eq_coe {α : Type u} [One α] {a : α} :
            1 = ↑a ↔ a = 1
            source
            @[simp]
            theorem WithBot.zero_eq_coe {α : Type u} [Zero α] {a : α} :
            0 = ↑a ↔ a = 0
            source
            @[simp]
            theorem WithBot.bot_ne_one {α : Type u} [One α] :
            ⊥ ≠ 1
            source
            @[simp]
            theorem WithBot.bot_ne_zero {α : Type u} [Zero α] :
            ⊥ ≠ 0
            source
            @[simp]
            theorem WithBot.one_ne_bot {α : Type u} [One α] :
            1 ≠ ⊥
            source
            @[simp]
            theorem WithBot.zero_ne_bot {α : Type u} [Zero α] :
            0 ≠ ⊥
            source
            @[simp]
            theorem WithBot.unbot_one {α : Type u} [One α] :
            unbot 1 ⋯ = 1
            source
            @[simp]
            theorem WithBot.unbot_zero {α : Type u} [Zero α] :
            unbot 0 ⋯ = 0
            source
            @[simp]
            theorem WithBot.unbotD_one {α : Type u} [One α] (d : α) :
            unbotD d 1 = 1
            source
            @[simp]
            theorem WithBot.unbotD_zero {α : Type u} [Zero α] (d : α) :
            unbotD d 0 = 0
            source
            @[simp]
            theorem WithBot.one_le_coe {α : Type u} [One α] {a : α} [LE α] :
            1 ≤ ↑a ↔ 1 ≤ a
            source
            @[simp]
            theorem WithBot.coe_nonneg {α : Type u} [Zero α] {a : α} [LE α] :
            0 ≤ ↑a ↔ 0 ≤ a
            source
            @[simp]
            theorem WithBot.coe_le_one {α : Type u} [One α] {a : α} [LE α] :
            ↑a ≤ 1 ↔ a ≤ 1
            source
            @[simp]
            theorem WithBot.coe_le_zero {α : Type u} [Zero α] {a : α} [LE α] :
            ↑a ≤ 0 ↔ a ≤ 0
            source
            @[simp]
            theorem WithBot.one_lt_coe {α : Type u} [One α] {a : α} [LT α] :
            1 < ↑a ↔ 1 < a
            source
            @[simp]
            theorem WithBot.coe_pos {α : Type u} [Zero α] {a : α} [LT α] :
            0 < ↑a ↔ 0 < a
            source
            @[simp]
            theorem WithBot.coe_lt_one {α : Type u} [One α] {a : α} [LT α] :
            ↑a < 1 ↔ a < 1
            source
            @[simp]
            theorem WithBot.coe_lt_zero {α : Type u} [Zero α] {a : α} [LT α] :
            ↑a < 0 ↔ a < 0
            source
            @[simp]
            theorem WithBot.bot_lt_one {α : Type u} [One α] [LT α] :
            ⊥ < 1
            source
            @[simp]
            theorem WithBot.bot_neg {α : Type u} [Zero α] [LT α] :
            ⊥ < 0
            source
            @[simp]
            theorem WithBot.map_one {α : Type u} [One α] {β : Type u_1} (f : α → β) :
            map f 1 = ↑(f 1)
            source
            @[simp]
            theorem WithBot.map_zero {α : Type u} [Zero α] {β : Type u_1} (f : α → β) :
            map f 0 = ↑(f 0)
            source
            theorem WithBot.map_eq_one_iff {β : Type v} {α : Type u_1} {f : α → β} {v : WithBot α} [One β] :
            map f v = 1 ↔ ∃ (x : α), v = ↑x ∧ f x = 1
            source
            theorem WithBot.map_eq_zero_iff {β : Type v} {α : Type u_1} {f : α → β} {v : WithBot α} [Zero β] :
            map f v = 0 ↔ ∃ (x : α), v = ↑x ∧ f x = 0
            source
            theorem WithBot.one_eq_map_iff {β : Type v} {α : Type u_1} {f : α → β} {v : WithBot α} [One β] :
            1 = map f v ↔ ∃ (x : α), v = ↑x ∧ f x = 1
            source
            theorem WithBot.zero_eq_map_iff {β : Type v} {α : Type u_1} {f : α → β} {v : WithBot α} [Zero β] :
            0 = map f v ↔ ∃ (x : α), v = ↑x ∧ f x = 0
            source
            instance WithBot.zeroLEOneClass {α : Type u} [One α] [Zero α] [LE α] [ZeroLEOneClass α] :
            ZeroLEOneClass (WithBot α)
            source
            @[instance_reducible]
            instance WithBot.add {α : Type u} [Add α] :
            Add (WithBot α)
            source
            @[simp]
            theorem WithBot.coe_add {α : Type u} [Add α] (a b : α) :
            ↑(a + b) = ↑a + ↑b
            source
            @[simp]
            theorem WithBot.bot_add {α : Type u} [Add α] (x : WithBot α) :
            ⊥ + x = ⊥
            source
            @[simp]
            theorem WithBot.add_bot {α : Type u} [Add α] (x : WithBot α) :
            x + ⊥ = ⊥
            source
            @[simp]
            theorem WithBot.add_eq_bot {α : Type u} [Add α] {x y : WithBot α} :
            x + y = ⊥ ↔ x = ⊥ ∨ y = ⊥
            source
            theorem WithBot.add_ne_bot {α : Type u} [Add α] {x y : WithBot α} :
            x + y ≠ ⊥ ↔ x ≠ ⊥ ∧ y ≠ ⊥
            source
            @[simp]
            theorem WithBot.bot_lt_add {α : Type u} [Add α] {x y : WithBot α} [LT α] :
            ⊥ < x + y ↔ ⊥ < x ∧ ⊥ < y
            source
            theorem WithBot.add_eq_coe {α : Type u} [Add α] {a b : WithBot α} {c : α} :
            a + b = ↑c ↔ ∃ (a' : α), ∃ (b' : α), ↑a' = a ∧ ↑b' = b ∧ a' + b' = c
            source
            theorem WithBot.add_coe_eq_bot_iff {α : Type u} [Add α] {x : WithBot α} {b : α} :
            x + ↑b = ⊥ ↔ x = ⊥
            source
            theorem WithBot.coe_add_eq_bot_iff {α : Type u} [Add α] {y : WithBot α} {a : α} :
            ↑a + y = ⊥ ↔ y = ⊥
            source
            theorem IsAddLeftRegular.withBot {α : Type u} [Add α] {a : α} (ha : IsAddLeftRegular a) :
            IsAddLeftRegular ↑a
            source
            theorem IsAddRightRegular.withBot {α : Type u} [Add α] {a : α} (ha : IsAddRightRegular a) :
            IsAddRightRegular ↑a
            source
            theorem AddLECancellable.withBot {α : Type u} [Add α] {a : α} [LE α] (ha : AddLECancellable a) :
            AddLECancellable ↑a
            source
            theorem WithBot.add_right_inj {α : Type u} [Add α] {x y z : WithBot α} [IsRightCancelAdd α] (hz : z ≠ ⊥) :
            x + z = y + z ↔ x = y
            source
            theorem WithBot.add_right_cancel {α : Type u} [Add α] {x y z : WithBot α} [IsRightCancelAdd α] (hz : z ≠ ⊥) (h : x + z = y + z) :
            x = y
            source
            theorem WithBot.add_left_inj {α : Type u} [Add α] {x y z : WithBot α} [IsLeftCancelAdd α] (hx : x ≠ ⊥) :
            x + y = x + z ↔ y = z
            source
            theorem WithBot.add_left_cancel {α : Type u} [Add α] {x y z : WithBot α} [IsLeftCancelAdd α] (hx : x ≠ ⊥) (h : x + y = x + z) :
            y = z
            source
            instance WithBot.addLeftMono {α : Type u} [Add α] [LE α] [AddLeftMono α] :
            AddLeftMono (WithBot α)
            source
            instance WithBot.addRightMono {α : Type u} [Add α] [LE α] [AddRightMono α] :
            AddRightMono (WithBot α)
            source
            instance WithBot.addLeftReflectLT {α : Type u} [Add α] [LT α] [AddLeftReflectLT α] :
            AddLeftReflectLT (WithBot α)
            source
            instance WithBot.addRightReflectLT {α : Type u} [Add α] [LT α] [AddRightReflectLT α] :
            AddRightReflectLT (WithBot α)
            source
            theorem WithBot.le_of_add_le_add_left {α : Type u} [Add α] {x y z : WithBot α} [LE α] [AddLeftReflectLE α] (hx : x ≠ ⊥) :
            x + y ≤ x + z → y ≤ z
            source
            theorem WithBot.le_of_add_le_add_right {α : Type u} [Add α] {x y z : WithBot α} [LE α] [AddRightReflectLE α] (hz : z ≠ ⊥) :
            x + z ≤ y + z → x ≤ y
            source
            theorem WithBot.add_lt_add_left {α : Type u} [Add α] {x y z : WithBot α} [LT α] [AddLeftStrictMono α] (hx : x ≠ ⊥) :
            y < z → x + y < x + z
            source
            theorem WithBot.add_lt_add_right {α : Type u} [Add α] {x y z : WithBot α} [LT α] [AddRightStrictMono α] (hz : z ≠ ⊥) :
            x < y → x + z < y + z
            source
            theorem WithBot.add_le_add_iff_left {α : Type u} [Add α] {x y z : WithBot α} [LE α] [AddLeftMono α] [AddLeftReflectLE α] (hx : x ≠ ⊥) :
            x + y ≤ x + z ↔ y ≤ z
            source
            theorem WithBot.add_le_add_iff_right {α : Type u} [Add α] {x y z : WithBot α} [LE α] [AddRightMono α] [AddRightReflectLE α] (hz : z ≠ ⊥) :
            x + z ≤ y + z ↔ x ≤ y
            source
            theorem WithBot.add_lt_add_iff_left {α : Type u} [Add α] {x y z : WithBot α} [LT α] [AddLeftStrictMono α] [AddLeftReflectLT α] (hx : x ≠ ⊥) :
            x + y < x + z ↔ y < z
            source
            theorem WithBot.add_lt_add_iff_right {α : Type u} [Add α] {x y z : WithBot α} [LT α] [AddRightStrictMono α] [AddRightReflectLT α] (hz : z ≠ ⊥) :
            x + z < y + z ↔ x < y
            source
            theorem WithBot.add_lt_add_of_le_of_lt {α : Type u} [Add α] {w x y z : WithBot α} [Preorder α] [AddLeftStrictMono α] [AddRightMono α] (hw : w ≠ ⊥) (hwy : w ≤ y) (hxz : x < z) :
            w + x < y + z
            source
            theorem WithBot.add_lt_add_of_lt_of_le {α : Type u} [Add α] {w x y z : WithBot α} [Preorder α] [AddLeftMono α] [AddRightStrictMono α] (hx : x ≠ ⊥) (hwy : w < y) (hxz : x ≤ z) :
            w + x < y + z
            source
            theorem WithBot.addLECancellable_of_ne_bot {α : Type u} [Add α] {x : WithBot α} [LE α] [AddLeftReflectLE α] (hx : x ≠ ⊥) :
            AddLECancellable x
            source
            theorem WithBot.addLECancellable_of_lt_bot {α : Type u} [Add α] {x : WithBot α} [Preorder α] [AddLeftReflectLE α] (hx : x < ⊥) :
            AddLECancellable x
            source
            theorem WithBot.addLECancellable_coe {α : Type u} [Add α] [LE α] [AddLeftReflectLE α] (a : α) :
            AddLECancellable ↑a
            source
            theorem WithBot.addLECancellable_iff_ne_bot {α : Type u} [Add α] {x : WithBot α} [Nonempty α] [Preorder α] [AddLeftReflectLE α] :
            AddLECancellable x ↔ x ≠ ⊥
            source
            theorem WithBot.add_le_add_iff_right' {α : Type u_1} [Add α] [LE α] [AddRightMono α] [AddRightReflectLE α] {a b c : WithBot (WithTop α)} (hc : c ≠ ⊥) (hc' : c ≠ ⊤) :
            a + c ≤ b + c ↔ a ≤ b

            Addition in WithBot (WithTop α) is right cancellative provided the element being cancelled is not ⊤ or ⊥.

            source
            @[simp]
            theorem WithBot.map_add {α : Type u} {β : Type v} [Add α] {F : Type u_1} [Add β] [FunLike F α β] [AddHomClass F α β] (f : F) (a b : WithBot α) :
            map (⇑f) (a + b) = map (⇑f) a + map (⇑f) b
            source
            @[instance_reducible]
            instance WithBot.addSemigroup {α : Type u} [AddSemigroup α] :
            AddSemigroup (WithBot α)
            source
            @[instance_reducible]
            instance WithBot.addCommSemigroup {α : Type u} [AddCommSemigroup α] :
            AddCommSemigroup (WithBot α)
            source
            @[instance_reducible]
            instance WithBot.addZeroClass {α : Type u} [AddZeroClass α] :
            AddZeroClass (WithBot α)
            source
            @[instance_reducible]
            instance WithBot.addMonoid {α : Type u} [AddMonoid α] :
            AddMonoid (WithBot α)
            source
            def WithBot.addHom {α : Type u} [AddMonoid α] :
            α →+ WithBot α

            Coercion from α to WithBot α as an AddMonoidHom.

            Instances For
              source
              @[simp]
              theorem WithBot.coe_addHom {α : Type u} [AddMonoid α] :
              ⇑addHom = some
              source
              @[simp]
              theorem WithBot.coe_nsmul {α : Type u} [AddMonoid α] (a : α) (n : ℕ) :
              ↑(n • a) = n • ↑a
              source
              @[instance_reducible]
              instance WithBot.addCommMonoid {α : Type u} [AddCommMonoid α] :
              AddCommMonoid (WithBot α)
              source
              @[instance_reducible]
              instance WithBot.instNatCast {α : Type u} [NatCast α] :
              NatCast (WithBot α)
              source
              @[simp]
              theorem WithBot.unbotD_natCast {α : Type u} [NatCast α] (d : α) (n : ℕ) :
              unbotD d ↑n = ↑n
              source
              @[simp]
              theorem WithTop.untopD_natCast {α : Type u} [NatCast α] (d : α) (n : ℕ) :
              untopD d ↑n = ↑n
              source
              @[simp]
              theorem WithBot.unbotD_ofNat {α : Type u} [NatCast α] (d : α) (n : ℕ) [n.AtLeastTwo] :
              unbotD d (OfNat.ofNat n) = OfNat.ofNat n
              source
              @[simp]
              theorem WithTop.untopD_ofNat {α : Type u} [NatCast α] (d : α) (n : ℕ) [n.AtLeastTwo] :
              untopD d (OfNat.ofNat n) = OfNat.ofNat n
              source
              @[instance_reducible]
              instance WithBot.addMonoidWithOne {α : Type u} [AddMonoidWithOne α] :
              AddMonoidWithOne (WithBot α)
              source
              theorem WithBot.coe_natCast {α : Type u} [AddMonoidWithOne α] (n : ℕ) :
              ↑↑n = ↑n
              source
              @[simp]
              theorem WithBot.natCast_ne_bot {α : Type u} [AddMonoidWithOne α] (n : ℕ) :
              ↑n ≠ ⊥
              source
              @[simp]
              theorem WithBot.bot_ne_natCast {α : Type u} [AddMonoidWithOne α] (n : ℕ) :
              ⊥ ≠ ↑n
              source
              @[simp]
              theorem WithBot.coe_ofNat {α : Type u} [AddMonoidWithOne α] (n : ℕ) [n.AtLeastTwo] :
              ↑(OfNat.ofNat n) = OfNat.ofNat n
              source
              @[simp]
              theorem WithBot.coe_eq_ofNat {α : Type u} [AddMonoidWithOne α] (n : ℕ) [n.AtLeastTwo] (m : α) :
              ↑m = OfNat.ofNat n ↔ m = OfNat.ofNat n
              source
              @[simp]
              theorem WithBot.ofNat_eq_coe {α : Type u} [AddMonoidWithOne α] (n : ℕ) [n.AtLeastTwo] (m : α) :
              OfNat.ofNat n = ↑m ↔ OfNat.ofNat n = m
              source
              @[simp]
              theorem WithBot.ofNat_ne_bot {α : Type u} [AddMonoidWithOne α] (n : ℕ) [n.AtLeastTwo] :
              OfNat.ofNat n ≠ ⊥
              source
              @[simp]
              theorem WithBot.bot_ne_ofNat {α : Type u} [AddMonoidWithOne α] (n : ℕ) [n.AtLeastTwo] :
              ⊥ ≠ OfNat.ofNat n
              source
              @[simp]
              theorem WithBot.map_ofNat {α : Type u} {β : Type v} [AddMonoidWithOne α] {f : α → β} (n : ℕ) [n.AtLeastTwo] :
              map f (OfNat.ofNat n) = ↑(f (OfNat.ofNat n))
              source
              @[simp]
              theorem WithBot.map_natCast {α : Type u} {β : Type v} [AddMonoidWithOne α] {f : α → β} (n : ℕ) :
              map f ↑n = ↑(f ↑n)
              source
              theorem WithBot.map_eq_ofNat_iff {α : Type u} {β : Type v} [AddMonoidWithOne α] {f : β → α} {n : ℕ} [n.AtLeastTwo] {a : WithBot β} :
              map f a = OfNat.ofNat n ↔ ∃ (x : β), a = ↑x ∧ f x = ↑n
              source
              theorem WithBot.ofNat_eq_map_iff {α : Type u} {β : Type v} [AddMonoidWithOne α] {f : β → α} {n : ℕ} [n.AtLeastTwo] {a : WithBot β} :
              OfNat.ofNat n = map f a ↔ ∃ (x : β), a = ↑x ∧ f x = ↑n
              source
              theorem WithBot.map_eq_natCast_iff {α : Type u} {β : Type v} [AddMonoidWithOne α] {f : β → α} {n : ℕ} {a : WithBot β} :
              map f a = ↑n ↔ ∃ (x : β), a = ↑x ∧ f x = ↑n
              source
              theorem WithBot.natCast_eq_map_iff {α : Type u} {β : Type v} [AddMonoidWithOne α] {f : β → α} {n : ℕ} {a : WithBot β} :
              ↑n = map f a ↔ ∃ (x : β), a = ↑x ∧ f x = ↑n
              source
              @[simp]
              theorem WithBot.bot_lt_natCast {α : Type u} [AddMonoidWithOne α] [LT α] (n : ℕ) :
              ⊥ < ↑n
              source
              instance WithBot.charZero {α : Type u} [AddMonoidWithOne α] [CharZero α] :
              CharZero (WithBot α)
              source
              @[instance_reducible]
              instance WithBot.addCommMonoidWithOne {α : Type u} [AddCommMonoidWithOne α] :
              AddCommMonoidWithOne (WithBot α)
              source
              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.

              Instances For
                source
                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

                Instances For
                  source
                  @[simp]
                  theorem OneHom.withBotMap_apply {M : Type u_1} {N : Type u_2} [One M] [One N] (f : OneHom M N) :
                  ⇑f.withBotMap = WithBot.map ⇑f
                  source
                  @[simp]
                  theorem ZeroHom.withBotMap_apply {M : Type u_1} {N : Type u_2} [Zero M] [Zero N] (f : ZeroHom M N) :
                  ⇑f.withBotMap = WithBot.map ⇑f
                  source
                  def AddHom.withBotMap {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : M →ₙ+ N) :
                  WithBot M →ₙ+ WithBot N

                  A version of WithBot.map for AddHoms.

                  Instances For
                    source
                    @[simp]
                    theorem AddHom.withBotMap_apply {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : M →ₙ+ N) :
                    ⇑f.withBotMap = WithBot.map ⇑f
                    source
                    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.

                    Instances For
                      source
                      @[simp]
                      theorem AddMonoidHom.withBotMap_apply {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) :
                      ⇑f.withBotMap = WithBot.map ⇑f
                      source
                      def AddEquiv.withBotCongr {α : Type u} {β : Type v} [Add α] [Add β] (e : α ≃+ β) :
                      WithBot α ≃+ WithBot β

                      A AddEquiv version of Equiv.withBotCongr.

                      Instances For
                        source
                        def AddEquiv.withTopCongr {α : Type u} {β : Type v} [Add α] [Add β] (e : α ≃+ β) :
                        WithTop α ≃+ WithTop β

                        A AddEquiv version of Equiv.withTopCongr.

                        Instances For
                          source
                          @[simp]
                          theorem AddEquiv.withTopCongr_apply {α : Type u} {β : Type v} [Add α] [Add β] (e : α ≃+ β) (a✝ : WithTop α) :
                          e.withTopCongr a✝ = WithTop.map (⇑e) a✝
                          source
                          @[simp]
                          theorem AddEquiv.withBotCongr_apply {α : Type u} {β : Type v} [Add α] [Add β] (e : α ≃+ β) (a✝ : WithBot α) :
                          e.withBotCongr a✝ = WithBot.map (⇑e) a✝
                          source
                          @[simp]
                          theorem AddEquiv.coe_withBotCongr {α : Type u} {β : Type v} [Add α] [Add β] (e : α ≃+ β) :
                          ⇑e.withBotCongr = WithBot.map ⇑e
                          source
                          @[simp]
                          theorem AddEquiv.coe_withTopCongr {α : Type u} {β : Type v} [Add α] [Add β] (e : α ≃+ β) :
                          ⇑e.withTopCongr = WithTop.map ⇑e
                          source
                          @[simp]
                          theorem AddEquiv.withBotCongr_toEquiv {α : Type u} {β : Type v} [Add α] [Add β] (e : α ≃+ β) :
                          ↑e.withBotCongr = (↑e).withBotCongr
                          source
                          @[simp]
                          theorem AddEquiv.withTopCongr_toEquiv {α : Type u} {β : Type v} [Add α] [Add β] (e : α ≃+ β) :
                          ↑e.withTopCongr = (↑e).withTopCongr
                          source
                          @[simp]
                          theorem AddEquiv.withBotCongr_toAddHom {α : Type u} {β : Type v} [Add α] [Add β] (e : α ≃+ β) :
                          ↑e.withBotCongr = (↑e).withBotMap
                          source
                          @[simp]
                          theorem AddEquiv.withTopCongr_toAddHom {α : Type u} {β : Type v} [Add α] [Add β] (e : α ≃+ β) :
                          ↑e.withTopCongr = (↑e).withBotMap
                          source
                          @[simp]
                          theorem AddEquiv.withBotCongr_refl {α : Type u} [Add α] :
                          (refl α).withBotCongr = refl (WithBot α)
                          source
                          @[simp]
                          theorem AddEquiv.withTopCongr_refl {α : Type u} [Add α] :
                          (refl α).withTopCongr = refl (WithTop α)
                          source
                          @[simp]
                          theorem AddEquiv.withBotCongr_symm {α : Type u} {β : Type v} [Add α] [Add β] (e : α ≃+ β) :
                          e.withBotCongr.symm = e.symm.withBotCongr
                          source
                          @[simp]
                          theorem AddEquiv.withTopCongr_symm {α : Type u} {β : Type v} [Add α] [Add β] (e : α ≃+ β) :
                          e.withTopCongr.symm = e.symm.withTopCongr
                          source
                          @[simp]
                          theorem AddEquiv.withBotCongr_trans {α : Type u} {β : Type v} {γ : Type u_1} [Add α] [Add β] [Add γ] (e₁ : α ≃+ β) (e₂ : β ≃+ γ) :
                          (e₁.trans e₂).withBotCongr = e₁.withBotCongr.trans e₂.withBotCongr
                          source
                          @[simp]
                          theorem AddEquiv.withTopCongr_trans {α : Type u} {β : Type v} {γ : Type u_1} [Add α] [Add β] [Add γ] (e₁ : α ≃+ β) (e₂ : β ≃+ γ) :
                          (e₁.trans e₂).withTopCongr = e₁.withTopCongr.trans e₂.withTopCongr