nsmul_mk — Mathlib

English

n times a nonnegative element applied under the mk construction yields the corresponding nonnegative element with nsmul nonneg preserved.

Русский

Умножение неотрицательного элемента на натуральное число через конструктор mk сохраняет неотрицательность.

LaTeX

$$$n \\cdot ⟨x, hx⟩ = ⟨n \\cdot x, nsmul\_nonneg hx n⟩$$$

Lean4

@[simp]
theorem nsmul_mk [AddMonoid α] [Preorder α] [AddLeftMono α] (n : ℕ) {x : α} (hx : 0 ≤ x) :
    (n • (⟨x, hx⟩ : { x : α // 0 ≤ x })) = ⟨n • x, nsmul_nonneg hx n⟩ :=
  rfl

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