smul_finset_subset_mul

Mathlib.Algebra.Group.Action.Pointwise.Finset

URI: https://scilib.ai/kg/mathlib#Finset.smul_finset_subset_mul

English

If a ∈ s, then a • t ⊆ s * t.

Русский

Если a принадлежит s, то a•t ⊆ s*t.

LaTeX

$$$a\in s\;\Rightarrow\; a\cdot t \subseteq s\cdot t.$$$

Lean4

@[to_additive]
theorem smul_finset_subset_mul : a ∈ s → a • t ⊆ s * t :=
  image_subset_image₂_right

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru