WithZero #
In this file we provide some basic API lemmas for the WithZero construction and we define
the morphism WithZeroMultInt.toNNReal.
Main Definitions #
WithZeroMultInt.toNNReal: TheMonoidWithZeroHomfromℤₘ₀ → ℝ≥0sending0 ↦ 0andx ↦ e^(Multiplicative.toAdd (WithZero.unzero hx)whenx ≠ 0, for a nonzeroe : ℝ≥0.
Main Results #
WithZeroMultInt.toNNReal_strictMono: The mapwithZeroMultIntToNNRealis strictly monotone whenever1 < e.
Tags #
WithZero, multiplicative, nnreal
Given a nonzero e : ℝ≥0, this is the map ℤₘ₀ → ℝ≥0 sending 0 ↦ 0 and
x ↦ e^(Multiplicative.toAdd (WithZero.unzero hx) when x ≠ 0 as a MonoidWithZeroHom.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
WithZeroMulInt.toNNReal_pos_apply
{e : NNReal}
(he : e ≠ 0)
{x : WithZero (Multiplicative ℤ)}
(hx : x = 0)
:
(WithZeroMulInt.toNNReal he) x = 0
theorem
WithZeroMulInt.toNNReal_neg_apply
{e : NNReal}
(he : e ≠ 0)
{x : WithZero (Multiplicative ℤ)}
(hx : x ≠ 0)
:
(WithZeroMulInt.toNNReal he) x = e ^ Multiplicative.toAdd (WithZero.unzero hx)
theorem
WithZeroMulInt.toNNReal_ne_zero
{e : NNReal}
{m : WithZero (Multiplicative ℤ)}
(he : e ≠ 0)
(hm : m ≠ 0)
:
(WithZeroMulInt.toNNReal he) m ≠ 0
toNNReal sends nonzero elements to nonzero elements.
theorem
WithZeroMulInt.toNNReal_pos
{e : NNReal}
{m : WithZero (Multiplicative ℤ)}
(he : e ≠ 0)
(hm : m ≠ 0)
:
0 < (WithZeroMulInt.toNNReal he) m
toNNReal sends nonzero elements to positive elements.
The map toNNReal is strictly monotone whenever 1 < e.
theorem
WithZeroMulInt.toNNReal_eq_one_iff
{e : NNReal}
(m : WithZero (Multiplicative ℤ))
(he0 : e ≠ 0)
(he1 : e ≠ 1)
:
(WithZeroMulInt.toNNReal he0) m = 1 ↔ m = 1
theorem
WithZeroMulInt.toNNReal_lt_one_iff
{e : NNReal}
{m : WithZero (Multiplicative ℤ)}
(he : 1 < e)
:
(WithZeroMulInt.toNNReal ⋯) m < 1 ↔ m < 1
theorem
WithZeroMulInt.toNNReal_le_one_iff
{e : NNReal}
{m : WithZero (Multiplicative ℤ)}
(he : 1 < e)
:
(WithZeroMulInt.toNNReal ⋯) m ≤ 1 ↔ m ≤ 1