ofScientific_nonneg — Mathlib

English

For any m, s, e, the rational of scientific notation Rat.ofScientific m s e is nonnegative.

Русский

Для любых m, s, e число Rat.ofScientific неотрицательно.

LaTeX

$$$$\\text{Rat.ofScientific}(m,s,e) \\ge 0.$$$$

Lean4

theorem ofScientific_nonneg (m : ℕ) (s : Bool) (e : ℕ) : 0 ≤ Rat.ofScientific m s e :=
  by
  rw [Rat.ofScientific]
  cases s
  · rw [if_neg (by decide)]
    refine num_nonneg.mp ?_
    rw [num_natCast]
    exact Int.natCast_nonneg _
  · rw [if_pos rfl, normalize_eq_mkRat]
    exact Rat.mkRat_nonneg (Int.natCast_nonneg _) _

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