Documentation

Mathlib.Algebra.Order.WithTop.Untop0

Conversion from WithTop to Base Type #

For types α that are instances of Zero, we provide a convenient conversion, WithTop.untop₀, that maps elements a : WithTop α to α, by mapping ⊤ to zero.

For settings where α has additional structure, we provide a large number of simplifier lemmas, akin to those that already exists for ENat.toNat.

source
def WithTop.untop₀ {α : Type u_1} [Zero α] (a : WithTop α) :
α

Conversion from WithTop α to α, mapping ⊤ to zero.

Equations
    Instances For

      Simplifying Lemmas in cases where α is an Instance of Zero #

      source
      @[simp]
      theorem WithTop.untop₀_eq_zero {α : Type u_1} [Zero α] {a : WithTop α} :
      a.untop₀ = 0 ↔ a = 0 ∨ a = ⊤
      source
      @[simp]
      theorem WithTop.untop₀_top {α : Type u_1} [Zero α] :
      ⊤.untop₀ = 0
      source
      @[simp]
      theorem WithTop.untop₀_zero {α : Type u_1} [Zero α] :
      untop₀ 0 = 0
      source
      @[simp]
      theorem WithTop.untop₀_coe {α : Type u_1} [Zero α] (a : α) :
      (↑a).untop₀ = a
      source
      theorem WithTop.coe_untop₀_of_ne_top {α : Type u_1} [Zero α] {a : WithTop α} (ha : a ≠ ⊤) :
      ↑a.untop₀ = a

      Simplifying Lemmas in cases where α is an AddMonoid #

      source
      @[simp]
      theorem WithTop.untopD_add {α : Type u_1} [Add α] {a b : WithTop α} {c : α} (ha : a ≠ ⊤) (hb : b ≠ ⊤) :
      untopD c (a + b) = untopD c a + untopD c b
      source
      @[simp]
      theorem WithTop.untop₀_add {α : Type u_1} [AddZeroClass α] {a b : WithTop α} (ha : a ≠ ⊤) (hb : b ≠ ⊤) :
      (a + b).untop₀ = a.untop₀ + b.untop₀

      Simplifying Lemmas in cases where α is a MulZeroClass #

      source
      @[simp]
      theorem WithTop.untop₀_mul {α : Type u_1} [DecidableEq α] [MulZeroClass α] (a b : WithTop α) :
      (a * b).untop₀ = a.untop₀ * b.untop₀

      Simplifying Lemmas in cases where α is a OrderedAddCommGroup #

      source
      @[simp]
      theorem WithTop.untop₀_nonneg {α : Type u_1} [AddCommGroup α] [PartialOrder α] {a : WithTop α} :
      0 ≤ a.untop₀ ↔ 0 ≤ a

      Elements of ordered additive commutative groups are nonnegative iff their untop₀ is nonnegative.

      Simplifying Lemmas in cases where α is a LinearOrderedAddCommGroup #

      source
      @[simp]
      theorem WithTop.untop₀_neg {α : Type u_1} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] (a : WithTop α) :
      (-a).untop₀ = -a.untop₀