mul_subset_mul — Mathlib

English

The product of the underlying sets satisfies (↑M : Set R) * (↑N : Set R) ⊆ (↑(M * N) : Set R).

Русский

Произведение множества M и множества N подпадает под множество M*N как подмножество: (↑M) · (↑N) ⊆ ↑(M*N).

LaTeX

$$$ (\uparrow M : Set R) * (\uparrow N : Set R) \subseteq (\uparrow (M * N) : Set R) $$$

Lean4

theorem mul_subset_mul : (↑M : Set R) * (↑N : Set R) ⊆ (↑(M * N) : Set R) :=
  smul_subset_smul

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