mkRat_nonpos — Mathlib

English

If a ≤ 0 for an integer a and any natural b, then a/b ≤ 0.

Русский

Если a ≤ 0 для целого a и любого натурального b, то a/b ≤ 0.

LaTeX

$$$\\forall a \\in \\mathbb{Z},\\ a \\le 0 \\Rightarrow \\forall b \\in \\mathbb{N},\\\\ b \\ge 0 \\Rightarrow \\dfrac{a}{b} \\le 0$$$

Lean4

theorem mkRat_nonpos {a : ℤ} (ha : a ≤ 0) (b : ℕ) : mkRat a b ≤ 0 :=
  by
  obtain rfl | hb := eq_or_ne b 0
  · simp
  · exact (mkRat_nonpos_iff a hb).mpr ha

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