smul_set_subset_smul

Mathlib.Algebra.Group.Pointwise.Set.Scalar

URI: https://scilib.ai/kg/mathlib#Set.smul_set_subset_smul

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_set_subset_smul {s : Set α} : a ∈ s → a • t ⊆ s • t :=
  image_subset_image2_right

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

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

Разделы

Аффилиация

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