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.

Equations

• a.untop₀ = WithTop.untopD 0 a

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

Simplifying Lemmas in cases where α is an AddMonoid

@[simp]

theorem WithTop.untopD_add {α : Type u_1} [AddMonoid α] {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} [AddMonoid α] {a b : WithTop α} (ha : a ≠ ⊤) (hb : b ≠ ⊤) : (a + b).untop₀ = a.untop₀ + b.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 a LinearOrderedAddCommGroup

@[simp]

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