cast_nonneg — Mathlib

English

If q is a nonnegative rational, then its image in α is nonnegative: 0 ≤ (q : α).

Русский

Если q — неотрицательная рациональная величина, то её образ в α неотрицателен: 0 ≤ (q : α).

LaTeX

$$$0 \\le (q : \\alpha)\\quad\\text{for all } q \\in \\mathbb{Q}_{\\ge 0}$$$

Lean4

theorem cast_nonneg (q : ℚ≥0) : 0 ≤ (q : α) := by rw [cast_def]; exact div_nonneg q.num.cast_nonneg q.den.cast_nonneg

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