toNNReal_eq_one_iff — Mathlib

English

If e ≠ 0 and e ≠ 1, then toNNReal e m = 1 holds iff m = 1.

Русский

Если e ≠ 0 и e ≠ 1, то toNNReal e m = 1 тогда и только если m = 1.

LaTeX

$$toNNReal(ne_zero_of_lt) m = 1 \Leftrightarrow m = 1$$

Lean4

theorem toNNReal_eq_one_iff {e : ℝ≥0} (m : ℤᵐ⁰) (he0 : e ≠ 0) (he1 : e ≠ 1) : toNNReal he0 m = 1 ↔ m = 1 :=
  by
  by_cases hm : m = 0
  · simp only [hm, map_zero, zero_ne_one]
  · refine ⟨fun h1 ↦ ?_, fun h1 ↦ h1 ▸ map_one _⟩
    rw [toNNReal_neg_apply he0 hm, zpow_eq_one_iff_right₀ (zero_le e) he1, toAdd_eq_zero] at h1
    rw [← WithZero.coe_unzero hm, h1, coe_one]

Похожие утверждения