mkRat_pos — Mathlib

English

Let a be an integer with a > 0 and b be a nonzero natural number. Then the rational number a/b is positive.

Русский

Пусть a ∈ ℤ с a > 0 и b ∈ ℕ, b ≠ 0. Тогда отношение a/b положительно.

LaTeX

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

Lean4

theorem mkRat_pos {a : ℤ} (ha : 0 < a) {b : ℕ} (hb : b ≠ 0) : 0 < mkRat a b :=
  (mkRat_pos_iff a hb).mpr ha

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