Documentation

Mathlib.Algebra.Order.Monoid.WithTop

Adjoining top/bottom elements to ordered monoids. #

source
instance WithTop.zero {α : Type u} [Zero α] :
Zero (WithTop α)
Equations
  • WithTop.zero = { zero := ↑0 }
source
instance WithTop.one {α : Type u} [One α] :
One (WithTop α)
Equations
  • WithTop.one = { one := ↑1 }
source
@[simp]
theorem WithTop.coe_zero {α : Type u} [Zero α] :
↑0 = 0
source
@[simp]
theorem WithTop.coe_one {α : Type u} [One α] :
↑1 = 1
source
@[simp]
theorem WithTop.coe_eq_zero {α : Type u} [Zero α] {a : α} :
↑a = 0 ↔ a = 0
source
@[simp]
theorem WithTop.coe_eq_one {α : Type u} [One α] {a : α} :
↑a = 1 ↔ a = 1
source
@[simp]
theorem WithTop.untop_zero {α : Type u} [Zero α] :
WithTop.untop 0 (_ : ↑0 ≠ ⊤) = 0
source
@[simp]
theorem WithTop.untop_one {α : Type u} [One α] :
WithTop.untop 1 (_ : ↑1 ≠ ⊤) = 1
source
@[simp]
theorem WithTop.untop_zero' {α : Type u} [Zero α] (d : α) :
WithTop.untop' d 0 = 0
source
@[simp]
theorem WithTop.untop_one' {α : Type u} [One α] (d : α) :
WithTop.untop' d 1 = 1
source
@[simp]
theorem WithTop.coe_nonneg {α : Type u} [Zero α] [LE α] {a : α} :
0 ≤ ↑a ↔ 0 ≤ a
source
@[simp]
theorem WithTop.one_le_coe {α : Type u} [One α] [LE α] {a : α} :
1 ≤ ↑a ↔ 1 ≤ a
source
@[simp]
theorem WithTop.coe_le_zero {α : Type u} [Zero α] [LE α] {a : α} :
↑a ≤ 0 ↔ a ≤ 0
source
@[simp]
theorem WithTop.coe_le_one {α : Type u} [One α] [LE α] {a : α} :
↑a ≤ 1 ↔ a ≤ 1
source
@[simp]
theorem WithTop.coe_pos {α : Type u} [Zero α] [LT α] {a : α} :
0 < ↑a ↔ 0 < a
source
@[simp]
theorem WithTop.one_lt_coe {α : Type u} [One α] [LT α] {a : α} :
1 < ↑a ↔ 1 < a
source
@[simp]
theorem WithTop.coe_lt_zero {α : Type u} [Zero α] [LT α] {a : α} :
↑a < 0 ↔ a < 0
source
@[simp]
theorem WithTop.coe_lt_one {α : Type u} [One α] [LT α] {a : α} :
↑a < 1 ↔ a < 1
source
@[simp]
theorem WithTop.map_zero {α : Type u} [Zero α] {β : Type u_1} (f : α → β) :
WithTop.map f 0 = ↑(f 0)
source
@[simp]
theorem WithTop.map_one {α : Type u} [One α] {β : Type u_1} (f : α → β) :
WithTop.map f 1 = ↑(f 1)
source
@[simp]
theorem WithTop.zero_eq_coe {α : Type u} [Zero α] {a : α} :
0 = ↑a ↔ a = 0
source
@[simp]
theorem WithTop.one_eq_coe {α : Type u} [One α] {a : α} :
1 = ↑a ↔ a = 1
source
@[simp]
theorem WithTop.top_ne_zero {α : Type u} [Zero α] :
⊤ ≠ 0
source
abbrev WithTop.top_ne_zero.match_1 {α : Type u_1} [Zero α] (motive : ⊤ = 0 → Prop) :
∀ (a : ⊤ = 0), motive a
Equations
  • (_ : motive a) = (_ : motive a)
Instances For
    source
    @[simp]
    theorem WithTop.top_ne_one {α : Type u} [One α] :
    ⊤ ≠ 1
    source
    @[simp]
    theorem WithTop.zero_ne_top {α : Type u} [Zero α] :
    0 ≠ ⊤
    source
    abbrev WithTop.zero_ne_top.match_1 {α : Type u_1} [Zero α] (motive : 0 = ⊤ → Prop) :
    ∀ (a : 0 = ⊤), motive a
    Equations
    • (_ : motive a) = (_ : motive a)
    Instances For
      source
      @[simp]
      theorem WithTop.one_ne_top {α : Type u} [One α] :
      1 ≠ ⊤
      source
      instance WithTop.zeroLEOneClass {α : Type u} [One α] [Zero α] [LE α] [ZeroLEOneClass α] :
      ZeroLEOneClass (WithTop α)
      Equations
      source
      instance WithTop.add {α : Type u} [Add α] :
      Add (WithTop α)
      Equations
      source
      theorem WithTop.coe_add {α : Type u} [Add α] {x : α} {y : α} :
      ↑(x + y) = ↑x + ↑y
      source
      @[deprecated]
      theorem WithTop.coe_bit0 {α : Type u} [Add α] {x : α} :
      ↑(bit0 x) = bit0 ↑x
      source
      @[deprecated]
      theorem WithTop.coe_bit1 {α : Type u} [Add α] [One α] {a : α} :
      ↑(bit1 a) = bit1 ↑a
      source
      @[simp]
      theorem WithTop.top_add {α : Type u} [Add α] (a : WithTop α) :
      ⊤ + a = ⊤
      source
      @[simp]
      theorem WithTop.add_top {α : Type u} [Add α] (a : WithTop α) :
      a + ⊤ = ⊤
      source
      @[simp]
      theorem WithTop.add_eq_top {α : Type u} [Add α] {a : WithTop α} {b : WithTop α} :
      a + b = ⊤ ↔ a = ⊤ ∨ b = ⊤
      source
      theorem WithTop.add_ne_top {α : Type u} [Add α] {a : WithTop α} {b : WithTop α} :
      a + b ≠ ⊤ ↔ a ≠ ⊤ ∧ b ≠ ⊤
      source
      theorem WithTop.add_lt_top {α : Type u} [Add α] [LT α] {a : WithTop α} {b : WithTop α} :
      a + b < ⊤ ↔ a < ⊤ ∧ b < ⊤
      source
      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
      source
      theorem WithTop.add_coe_eq_top_iff {α : Type u} [Add α] {x : WithTop α} {y : α} :
      x + ↑y = ⊤ ↔ x = ⊤
      source
      theorem WithTop.coe_add_eq_top_iff {α : Type u} [Add α] {x : α} {y : WithTop α} :
      ↑x + y = ⊤ ↔ y = ⊤
      source
      theorem WithTop.add_right_cancel_iff {α : Type u} [Add α] {a : WithTop α} {b : WithTop α} {c : WithTop α} [IsRightCancelAdd α] (ha : a ≠ ⊤) :
      b + a = c + a ↔ b = c
      source
      theorem WithTop.add_right_cancel {α : Type u} [Add α] {a : WithTop α} {b : WithTop α} {c : WithTop α} [IsRightCancelAdd α] (ha : a ≠ ⊤) (h : b + a = c + a) :
      b = c
      source
      theorem WithTop.add_left_cancel_iff {α : Type u} [Add α] {a : WithTop α} {b : WithTop α} {c : WithTop α} [IsLeftCancelAdd α] (ha : a ≠ ⊤) :
      a + b = a + c ↔ b = c
      source
      theorem WithTop.add_left_cancel {α : Type u} [Add α] {a : WithTop α} {b : WithTop α} {c : WithTop α} [IsLeftCancelAdd α] (ha : a ≠ ⊤) (h : a + b = a + c) :
      b = c
      source
      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 : WithTop α) => x + x_1) fun (x x_1 : WithTop α) => x ≤ x_1
      Equations
      • One or more equations did not get rendered due to their size.
      source
      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 : WithTop α) => x + x_1) fun (x x_1 : WithTop α) => x ≤ x_1
      Equations
      • One or more equations did not get rendered due to their size.
      source
      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 : WithTop α) => x + x_1) fun (x x_1 : WithTop α) => x < x_1
      Equations
      • One or more equations did not get rendered due to their size.
      source
      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 : WithTop α) => x + x_1) fun (x x_1 : WithTop α) => x < x_1
      Equations
      • One or more equations did not get rendered due to their size.
      source
      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
      source
      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
      source
      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
      source
      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
      source
      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
      source
      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
      source
      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
      source
      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
      source
      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
      source
      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
      source
      @[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
      source
      instance WithTop.addSemigroup {α : Type u} [AddSemigroup α] :
      AddSemigroup (WithTop α)
      Equations
      • One or more equations did not get rendered due to their size.
      source
      instance WithTop.addCommSemigroup {α : Type u} [AddCommSemigroup α] :
      AddCommSemigroup (WithTop α)
      Equations
      • One or more equations did not get rendered due to their size.
      source
      instance WithTop.addZeroClass {α : Type u} [AddZeroClass α] :
      AddZeroClass (WithTop α)
      Equations
      • One or more equations did not get rendered due to their size.
      source
      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
      source
      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)
      source
      instance WithTop.addMonoidWithOne {α : Type u} [AddMonoidWithOne α] :
      AddMonoidWithOne (WithTop α)
      Equations
      • WithTop.addMonoidWithOne = let src := WithTop.one; let src_1 := WithTop.addMonoid; AddMonoidWithOne.mk
      source
      instance WithTop.charZero {α : Type u} [AddMonoidWithOne α] [CharZero α] :
      CharZero (WithTop α)
      Equations
      source
      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)
      source
      instance WithTop.orderedAddCommMonoid {α : Type u} [OrderedAddCommMonoid α] :
      OrderedAddCommMonoid (WithTop α)
      Equations
      source
      instance WithTop.linearOrderedAddCommMonoidWithTop {α : Type u} [LinearOrderedAddCommMonoid α] :
      LinearOrderedAddCommMonoidWithTop (WithTop α)
      Equations
      • One or more equations did not get rendered due to their size.
      source
      instance WithTop.existsAddOfLE {α : Type u} [LE α] [Add α] [ExistsAddOfLE α] :
      ExistsAddOfLE (WithTop α)
      Equations
      source
      instance WithTop.canonicallyOrderedAddCommMonoid {α : Type u} [CanonicallyOrderedAddCommMonoid α] :
      CanonicallyOrderedAddCommMonoid (WithTop α)
      Equations
      • One or more equations did not get rendered due to their size.
      source
      instance WithTop.instCanonicallyLinearOrderedAddCommMonoidWithTop {α : Type u} [CanonicallyLinearOrderedAddCommMonoid α] :
      CanonicallyLinearOrderedAddCommMonoid (WithTop α)
      Equations
      • One or more equations did not get rendered due to their size.
      source
      @[simp]
      theorem WithTop.coe_nat {α : Type u} [AddMonoidWithOne α] (n : ℕ) :
      ↑↑n = ↑n
      source
      @[simp]
      theorem WithTop.nat_ne_top {α : Type u} [AddMonoidWithOne α] (n : ℕ) :
      ↑n ≠ ⊤
      source
      @[simp]
      theorem WithTop.top_ne_nat {α : Type u} [AddMonoidWithOne α] (n : ℕ) :
      ⊤ ≠ ↑n
      source
      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.
      Instances For
        source
        @[simp]
        theorem WithTop.zero_lt_top {α : Type u} [OrderedAddCommMonoid α] :
        0 < ⊤
        source
        theorem WithTop.zero_lt_coe {α : Type u} [OrderedAddCommMonoid α] (a : α) :
        0 < ↑a ↔ 0 < a
        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

        Equations
        Instances For
          source
          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
          source
          @[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
          source
          @[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
          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.

          Equations
          Instances For
            source
            @[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
            source
            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
            Instances For
              source
              @[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
              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.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                instance WithBot.zero {α : Type u} [Zero α] :
                Zero (WithBot α)
                Equations
                • WithBot.zero = WithTop.zero
                source
                instance WithBot.one {α : Type u} [One α] :
                One (WithBot α)
                Equations
                • WithBot.one = WithTop.one
                source
                instance WithBot.add {α : Type u} [Add α] :
                Add (WithBot α)
                Equations
                • WithBot.add = WithTop.add
                source
                instance WithBot.AddSemigroup {α : Type u} [AddSemigroup α] :
                AddSemigroup (WithBot α)
                Equations
                • WithBot.AddSemigroup = WithTop.addSemigroup
                source
                instance WithBot.addCommSemigroup {α : Type u} [AddCommSemigroup α] :
                AddCommSemigroup (WithBot α)
                Equations
                • WithBot.addCommSemigroup = WithTop.addCommSemigroup
                source
                instance WithBot.addZeroClass {α : Type u} [AddZeroClass α] :
                AddZeroClass (WithBot α)
                Equations
                • WithBot.addZeroClass = WithTop.addZeroClass
                source
                instance WithBot.addMonoid {α : Type u} [AddMonoid α] :
                AddMonoid (WithBot α)
                Equations
                • WithBot.addMonoid = WithTop.addMonoid
                source
                instance WithBot.addCommMonoid {α : Type u} [AddCommMonoid α] :
                AddCommMonoid (WithBot α)
                Equations
                • WithBot.addCommMonoid = WithTop.addCommMonoid
                source
                instance WithBot.addMonoidWithOne {α : Type u} [AddMonoidWithOne α] :
                AddMonoidWithOne (WithBot α)
                Equations
                • WithBot.addMonoidWithOne = WithTop.addMonoidWithOne
                source
                instance WithBot.charZero {α : Type u} [AddMonoidWithOne α] [CharZero α] :
                CharZero (WithBot α)
                Equations
                source
                instance WithBot.addCommMonoidWithOne {α : Type u} [AddCommMonoidWithOne α] :
                AddCommMonoidWithOne (WithBot α)
                Equations
                • WithBot.addCommMonoidWithOne = WithTop.addCommMonoidWithOne
                source
                instance WithBot.zeroLEOneClass {α : Type u} [Zero α] [One α] [LE α] [ZeroLEOneClass α] :
                ZeroLEOneClass (WithBot α)
                Equations
                source
                theorem WithBot.coe_zero {α : Type u} [Zero α] :
                ↑0 = 0
                source
                theorem WithBot.coe_one {α : Type u} [One α] :
                ↑1 = 1
                source
                theorem WithBot.coe_eq_zero {α : Type u} [Zero α] {a : α} :
                ↑a = 0 ↔ a = 0
                source
                theorem WithBot.coe_eq_one {α : Type u} [One α] {a : α} :
                ↑a = 1 ↔ a = 1
                source
                @[simp]
                theorem WithBot.unbot_zero {α : Type u} [Zero α] :
                WithBot.unbot 0 (_ : ↑0 ≠ ⊥) = 0
                source
                @[simp]
                theorem WithBot.unbot_one {α : Type u} [One α] :
                WithBot.unbot 1 (_ : ↑1 ≠ ⊥) = 1
                source
                @[simp]
                theorem WithBot.unbot_zero' {α : Type u} [Zero α] (d : α) :
                WithBot.unbot' d 0 = 0
                source
                @[simp]
                theorem WithBot.unbot_one' {α : Type u} [One α] (d : α) :
                WithBot.unbot' d 1 = 1
                source
                @[simp]
                theorem WithBot.coe_nonneg {α : Type u} [Zero α] [LE α] {a : α} :
                0 ≤ ↑a ↔ 0 ≤ a
                source
                @[simp]
                theorem WithBot.one_le_coe {α : Type u} [One α] [LE α] {a : α} :
                1 ≤ ↑a ↔ 1 ≤ a
                source
                @[simp]
                theorem WithBot.coe_le_zero {α : Type u} [Zero α] [LE α] {a : α} :
                ↑a ≤ 0 ↔ a ≤ 0
                source
                @[simp]
                theorem WithBot.coe_le_one {α : Type u} [One α] [LE α] {a : α} :
                ↑a ≤ 1 ↔ a ≤ 1
                source
                @[simp]
                theorem WithBot.coe_pos {α : Type u} [Zero α] [LT α] {a : α} :
                0 < ↑a ↔ 0 < a
                source
                @[simp]
                theorem WithBot.one_lt_coe {α : Type u} [One α] [LT α] {a : α} :
                1 < ↑a ↔ 1 < a
                source
                @[simp]
                theorem WithBot.coe_lt_zero {α : Type u} [Zero α] [LT α] {a : α} :
                ↑a < 0 ↔ a < 0
                source
                @[simp]
                theorem WithBot.coe_lt_one {α : Type u} [One α] [LT α] {a : α} :
                ↑a < 1 ↔ a < 1
                source
                @[simp]
                theorem WithBot.map_zero {α : Type u} {β : Type u_1} [Zero α] (f : α → β) :
                WithBot.map f 0 = ↑(f 0)
                source
                @[simp]
                theorem WithBot.map_one {α : Type u} {β : Type u_1} [One α] (f : α → β) :
                WithBot.map f 1 = ↑(f 1)
                source
                theorem WithBot.coe_nat {α : Type u} [AddMonoidWithOne α] (n : ℕ) :
                ↑↑n = ↑n
                source
                @[simp]
                theorem WithBot.nat_ne_bot {α : Type u} [AddMonoidWithOne α] (n : ℕ) :
                ↑n ≠ ⊥
                source
                @[simp]
                theorem WithBot.bot_ne_nat {α : Type u} [AddMonoidWithOne α] (n : ℕ) :
                ⊥ ≠ ↑n
                source
                theorem WithBot.coe_add {α : Type u} [Add α] (a : α) (b : α) :
                ↑(a + b) = ↑a + ↑b
                source
                @[deprecated]
                theorem WithBot.coe_bit0 {α : Type u} [Add α] {x : α} :
                ↑(bit0 x) = bit0 ↑x
                source
                @[deprecated]
                theorem WithBot.coe_bit1 {α : Type u} [Add α] [One α] {a : α} :
                ↑(bit1 a) = bit1 ↑a
                source
                @[simp]
                theorem WithBot.bot_add {α : Type u} [Add α] (a : WithBot α) :
                ⊥ + a = ⊥
                source
                @[simp]
                theorem WithBot.add_bot {α : Type u} [Add α] (a : WithBot α) :
                a + ⊥ = ⊥
                source
                @[simp]
                theorem WithBot.add_eq_bot {α : Type u} [Add α] {a : WithBot α} {b : WithBot α} :
                a + b = ⊥ ↔ a = ⊥ ∨ b = ⊥
                source
                theorem WithBot.add_ne_bot {α : Type u} [Add α] {a : WithBot α} {b : WithBot α} :
                a + b ≠ ⊥ ↔ a ≠ ⊥ ∧ b ≠ ⊥
                source
                theorem WithBot.bot_lt_add {α : Type u} [Add α] [LT α] {a : WithBot α} {b : WithBot α} :
                ⊥ < a + b ↔ ⊥ < a ∧ ⊥ < b
                source
                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
                source
                theorem WithBot.add_coe_eq_bot_iff {α : Type u} [Add α] {a : WithBot α} {y : α} :
                a + ↑y = ⊥ ↔ a = ⊥
                source
                theorem WithBot.coe_add_eq_bot_iff {α : Type u} [Add α] {b : WithBot α} {x : α} :
                ↑x + b = ⊥ ↔ b = ⊥
                source
                theorem WithBot.add_right_cancel_iff {α : Type u} [Add α] {a : WithBot α} {b : WithBot α} {c : WithBot α} [IsRightCancelAdd α] (ha : a ≠ ⊥) :
                b + a = c + a ↔ b = c
                source
                theorem WithBot.add_right_cancel {α : Type u} [Add α] {a : WithBot α} {b : WithBot α} {c : WithBot α} [IsRightCancelAdd α] (ha : a ≠ ⊥) (h : b + a = c + a) :
                b = c
                source
                theorem WithBot.add_left_cancel_iff {α : Type u} [Add α] {a : WithBot α} {b : WithBot α} {c : WithBot α} [IsLeftCancelAdd α] (ha : a ≠ ⊥) :
                a + b = a + c ↔ b = c
                source
                theorem WithBot.add_left_cancel {α : Type u} [Add α] {a : WithBot α} {b : WithBot α} {c : WithBot α} [IsLeftCancelAdd α] (ha : a ≠ ⊥) (h : a + b = a + c) :
                b = c
                source
                @[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
                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

                Equations
                Instances For
                  source
                  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
                  source
                  @[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
                  source
                  @[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
                  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.

                  Equations
                  Instances For
                    source
                    @[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
                    source
                    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
                    Instances For
                      source
                      @[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
                      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.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        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 : WithBot α) => x + x_1) fun (x x_1 : WithBot α) => x ≤ x_1
                        Equations
                        • One or more equations did not get rendered due to their size.
                        source
                        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 : WithBot α) => x + x_1) fun (x x_1 : WithBot α) => x ≤ x_1
                        Equations
                        • One or more equations did not get rendered due to their size.
                        source
                        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 : WithBot α) => x + x_1) fun (x x_1 : WithBot α) => x < x_1
                        Equations
                        • One or more equations did not get rendered due to their size.
                        source
                        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 : WithBot α) => x + x_1) fun (x x_1 : WithBot α) => x < x_1
                        Equations
                        • One or more equations did not get rendered due to their size.
                        source
                        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
                        source
                        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
                        source
                        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
                        source
                        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
                        source
                        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
                        source
                        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
                        source
                        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
                        source
                        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
                        source
                        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
                        source
                        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
                        source
                        instance WithBot.orderedAddCommMonoid {α : Type u} [OrderedAddCommMonoid α] :
                        OrderedAddCommMonoid (WithBot α)
                        Equations
                        • One or more equations did not get rendered due to their size.
                        source
                        instance WithBot.linearOrderedAddCommMonoid {α : Type u} [LinearOrderedAddCommMonoid α] :
                        LinearOrderedAddCommMonoid (WithBot α)
                        Equations
                        • One or more equations did not get rendered due to their size.