smul_set_subset_iff

Mathlib.Algebra.Group.Pointwise.Set.Scalar

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

English

a · s ⊆ t iff ∀ b, b ∈ s implies a · b ∈ t

Русский

a · s ⊆ t эквивалентно ∀ b, b ∈ s → a · b ∈ t

LaTeX

$$$ a \\cdot s \\subseteq t \\iff \\forall b,\\ b \\in s \\rightarrow a \\cdot b \\in t $$$

Lean4

@[to_additive]
theorem smul_set_subset_iff : a • s ⊆ t ↔ ∀ ⦃b⦄, b ∈ s → a • b ∈ t :=
  image_subset_iff

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

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

Разделы

Аффилиация

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