smul_subset_smul_right — Mathlib

English

Let s1 and s2 be finite subsets of a type and t a finite subset of another type, with an action by scalars. If s1 is contained in s2, then the scalar product s1 • t is contained in s2 • t.

Русский

Пусть s1, s2 — конечные множества в одной группе, t — конечное множество, действием которого является умножение скаляром. Тогда если s1 ⊆ s2, то s1 • t ⊆ s2 • t.

LaTeX

$$$s_1 \subseteq s_2 \implies s_1 \cdot t \subseteq s_2 \cdot t$$$

Lean4

@[to_additive]
theorem smul_subset_smul_right : s₁ ⊆ s₂ → s₁ • t ⊆ s₂ • t :=
  image₂_subset_right

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