coe_mul — Mathlib

English

The inclusion map preserves multiplication: the underlying set of the product equals the product of underlying sets: (S * T) as a set equals S * T.

Русский

Встраиваемая карта сохраняет умножение: множество-носитель произведения равно произведению множеств носителей.

LaTeX

$$$(\\uparrow(S * T) : Set \\alpha) = S * T$$$

Lean4

@[to_additive (attr := simp, norm_cast)]
theorem coe_mul (s t : UpperSet α) : (↑(s * t) : Set α) = s * t :=
  rfl

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