instNNRatSMul — Mathlib

English

There is a SMul action of ℚ≥0 on the nonnegative subtype, i.e., q • a ∈ { x ≥ 0 } for q ∈ ℚ≥0 and a ∈ { x ≥ 0 }.

Русский

Существует действие умножения на ℚ≥0 на неотрицательном подтипе: q • a ∈ { x ≥ 0 } для q ∈ ℚ≥0 и a ∈ { x ≥ 0 }.

LaTeX

$$$\\forall q \\in \\mathbb{Q}_{\\ge 0}, \\; \\forall a \\in { x : α // 0 ≤ x }, \\; q \\cdot a \\in { x : α // 0 ≤ x }$$$

Lean4

instance instNNRatSMul : SMul ℚ≥0 { x : α // 0 ≤ x } where
  smul q a := ⟨q • a, by rw [NNRat.smul_def]; exact mul_nonneg q.cast_nonneg a.2⟩

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