mk_mul_mk — Mathlib

English

Multiplication on the subtype is defined by multiplying the representatives: the product of ⟨x, hx⟩ and ⟨y, hy⟩ is ⟨x⋅y, mul_nonneg hx hy⟩.

Русский

Умножение на подтипе задаётся как произведение представителей: произведение ⟨x, hx⟩ и ⟨y, hy⟩ равно ⟨xy, mul_nonneg hx hy⟩.

LaTeX

$$$ (\langle x, h_x \rangle) * (\langle y, h_y \rangle) = \langle x y, mul\_nonneg\, h_x\, h_y \rangle $$$

Lean4

@[simp]
theorem mk_mul_mk {x y : α} (hx : 0 ≤ x) (hy : 0 ≤ y) :
    (⟨x, hx⟩ : { x : α // 0 ≤ x }) * ⟨y, hy⟩ = ⟨x * y, mul_nonneg hx hy⟩ :=
  rfl

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