vsub_subset_vsub_right

Mathlib.Algebra.Group.Pointwise.Set.Scalar

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

English

If s1 ⊆ s2 then s1 −ᵥ t ⊆ s2 −ᵥ t.

Русский

Если s1 ⊆ s2, то s1 −ᵥ t ⊆ s2 −ᵥ t.

LaTeX

$$$ s1 \subseteq s2 \Rightarrow s1 -ᵥ t \subseteq s2 -ᵥ t $$$

Lean4

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

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

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

Разделы

Аффилиация

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