qsmul_of_nonneg — Mathlib

English

If a ≥ 0 then a • x equals the nonnegative rational action ⟨a, h⟩ on x.

Русский

Если $a \\ge 0$, то $a\\cdot x$ равняется действию неотрицательного рационального числа, применённому к $x$.

LaTeX

$$$a\\ge 0 \\Rightarrow a\\cdot x = (\\langle a, h\\rangle)\\cdot x$, где $h$ подтверждает неотрицательность $a$.$$

Lean4

theorem qsmul_of_nonneg {a : ℚ} (h : 0 ≤ a) (x : DivisibleHull M) : a • x = (show ℚ≥0 from ⟨a, h⟩) • x :=
  by
  have := h.eq_or_lt
  aesop (add simp [qsmul_def, abs_of_pos])

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