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 involving addition and negation #

    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₀
    source
    @[simp]
    theorem WithTop.untop₀_natCast {α : Type u_1} [AddMonoidWithOne α] (n : ℕ) :
    (↑n).untop₀ = ↑n
    source
    @[simp]
    theorem WithTop.untop₀_one {α : Type u_2} [AddMonoidWithOne α] :
    untop₀ 1 = 1
    source
    @[simp]
    theorem WithTop.untop₀_ofNat {α : Type u_1} [AddMonoidWithOne α] (n : ℕ) [n.AtLeastTwo] :
    (OfNat.ofNat n).untop₀ = OfNat.ofNat n
    source
    @[simp]
    theorem WithTop.untop₀_neg {α : Type u_1} [AddCommGroup α] (a : WithTop α) :
    (-a).untop₀ = -a.untop₀
    source
    @[simp]
    theorem WithTop.untop₀_mul {α : Type u_1} [DecidableEq α] [MulZeroClass α] (a b : WithTop α) :
    (a * b).untop₀ = a.untop₀ * b.untop₀
    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.

    source
    theorem WithTop.le_of_untop₀_le_untop₀ {α : Type u_1} [AddCommGroup α] [PartialOrder α] {a b : WithTop α} (ha : a ≠ ⊤) (h : a.untop₀ ≤ b.untop₀) :
    a ≤ b
    source
    @[simp]
    theorem WithTop.untop₀_le_untop₀ {α : Type u_1} [AddCommGroup α] [PartialOrder α] {a b : WithTop α} (hb : b ≠ ⊤) (h : a ≤ b) :
    a.untop₀ ≤ b.untop₀
    source
    theorem WithTop.untop₀_le_untop₀_iff {α : Type u_1} [AddCommGroup α] [PartialOrder α] {a b : WithTop α} (ha : a ≠ ⊤) (hb : b ≠ ⊤) :
    a.untop₀ ≤ b.untop₀ ↔ a ≤ b
    source
    @[simp]
    theorem WithTop.untop₀_max {α : Type u_1} [AddCommGroup α] [LinearOrder α] {a b : WithTop α} (ha : a ≠ ⊤) (hb : b ≠ ⊤) :
    (max a b).untop₀ = max a.untop₀ b.untop₀
    source
    @[simp]
    theorem WithTop.untop₀_min {α : Type u_1} [AddCommGroup α] [LinearOrder α] {a b : WithTop α} (ha : a ≠ ⊤) (hb : b ≠ ⊤) :
    (min a b).untop₀ = min a.untop₀ b.untop₀