mkRat_nonpos_iff — Mathlib

English

For an integer a and a nonzero natural b, the rational a/b is nonpositive if and only if a ≤ 0.

Русский

Для целого a и не нулевого натурального b число a/b не положительно тогда и только тогда, когда a ≤ 0.

LaTeX

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

Lean4

theorem mkRat_nonpos_iff (a : ℤ) {b : ℕ} (hb : b ≠ 0) : mkRat a b ≤ 0 ↔ a ≤ 0 := by grind [lt_iff_not_ge, mkRat_pos_iff]

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