vsub_subset_vsub_right

Mathlib.Algebra.Group.Pointwise.Finset.Scalar

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

English

s1 ⊆ s2 implies s1 -ᵥ t ⊆ s2 -ᵥ t.

Русский

s1 ⊆ s2 тогда s1 -ᵥ t ⊆ s2 -ᵥ t.

LaTeX

$$$ s_1 \subseteq s_2 \rightarrow s_1 -ᵥ t \subseteq s_2 -ᵥ t $$$

Lean4

theorem vsub_subset_vsub_right : s₁ ⊆ s₂ → s₁ -ᵥ t ⊆ s₂ -ᵥ t :=
  image₂_subset_right

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

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

Разделы

Аффилиация

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