instMulNonemptyInterval — Mathlib

English

Assuming a preorder on α and a multiplication that is monotone on both sides, NonemptyInterval α inherits a multiplication by defining (s * t) through endpointwise multiplication of s and t: the endpoints of s * t are (fst s)(fst t) and (snd s)(snd t).

Русский

Пусть на α задан предorder и умножение, монотонное слева и справа; тогда NonemptyInterval α имеет умножение, задаваемое покоординатно: (s · t).fst = s.fst · t.fst, (s · t).snd = s.snd · t.snd.

LaTeX

$$$\\forall s,t:\\mathrm{NonemptyInterval}(\\alpha),\\ (s * t).toProd = s.toProd * t.toProd$$$

Lean4

@[to_additive]
instance : Mul (NonemptyInterval α) :=
  ⟨fun s t => ⟨s.toProd * t.toProd, mul_le_mul' s.fst_le_snd t.fst_le_snd⟩⟩

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