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.

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

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

Simplifying Lemmas in cases where α is an Instance of Zero

@[simp]

theorem WithTop.untop₀_eq_zero {α : Type u_1} [Zero α] {a : WithTop α} : a.untop₀ = 0 ↔ a = 0 ∨ a = ⊤

@[simp]

theorem WithTop.untop₀_top {α : Type u_1} [Zero α] : ⊤.untop₀ = 0

@[simp]

theorem WithTop.untop₀_zero {α : Type u_1} [Zero α] : untop₀ 0 = 0

@[simp]

theorem WithTop.untop₀_coe {α : Type u_1} [Zero α] (a : α) : (↑a).untop₀ = a

theorem WithTop.coe_untop₀_of_ne_top {α : Type u_1} [Zero α] {a : WithTop α} (ha : a ≠ ⊤) : ↑a.untop₀ = a

Simplifying Lemmas involving addition and negation

@[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

@[simp]

theorem WithTop.untop₀_add {α : Type u_1} [AddZeroClass α] {a b : WithTop α} (ha : a ≠ ⊤) (hb : b ≠ ⊤) : (a + b).untop₀ = a.untop₀ + b.untop₀

@[simp]

theorem WithTop.untop₀_natCast {α : Type u_1} [AddMonoidWithOne α] (n : ℕ) : (↑n).untop₀ = ↑n

@[simp]

theorem WithTop.untop₀_ofNat {α : Type u_1} [AddMonoidWithOne α] (n : ℕ) [n.AtLeastTwo] : (OfNat.ofNat n).untop₀ = OfNat.ofNat n

@[simp]

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

Simplifying Lemmas in cases where α is a MulZeroClass

@[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 an OrderedAddCommGroup

@[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.

theorem WithTop.le_of_untop₀_le_untop₀ {α : Type u_1} [AddCommGroup α] [PartialOrder α] {a b : WithTop α} (ha : a ≠ ⊤) (h : a.untop₀ ≤ b.untop₀) : a ≤ b

@[simp]

theorem WithTop.untop₀_le_untop₀ {α : Type u_1} [AddCommGroup α] [PartialOrder α] {a b : WithTop α} (hb : b ≠ ⊤) (h : a ≤ b) : a.untop₀ ≤ b.untop₀

theorem WithTop.untop₀_le_untop₀_iff {α : Type u_1} [AddCommGroup α] [PartialOrder α] {a b : WithTop α} (ha : a ≠ ⊤) (hb : b ≠ ⊤) : a.untop₀ ≤ b.untop₀ ↔ a ≤ b

Simplifying Lemmas in cases where α is a LinearOrderedAddCommGroup

@[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₀

@[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₀