mk_nnqsmul — Mathlib

English

Identical to mk_nnqsmul: for q ∈ ℚ≥0 and a ≥ 0, the subtype element q • a equals the ambient scalar multiple.

Русский

То же, что и mk_nnqsmul: для q ∈ ℚ≥0 и a ≥ 0, элемент ⟨q • a, …⟩ равен q • a.

LaTeX

$$$\\forall q \\in \\mathbb{Q}_{\\ge 0},\\; \\forall a \\ge 0:\\; (\\langle q \\cdot a, h\\rangle) = q \\cdot a$$$

Lean4

@[simp]
theorem mk_nnqsmul (q : ℚ≥0) (a : α) (ha : 0 ≤ a) :
    (⟨q • a, by rw [NNRat.smul_def]; exact mul_nonneg q.cast_nonneg ha⟩ : { x : α // 0 ≤ x }) = q • a :=
  rfl

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