vsub_subset_vsub

Mathlib.Algebra.Group.Pointwise.Set.Scalar

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

English

If s1 ⊆ s2 and t1 ⊆ t2, then s1 −ᵥ t1 ⊆ s2 −ᵥ t2.

Русский

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

LaTeX

$$$ s1 \subseteq s2 \ \land \ t1 \subseteq t2 \Rightarrow s1 -ᵥ t1 \subseteq s2 -ᵥ t2 $$$

Lean4

@[mono, gcongr]
theorem vsub_subset_vsub : s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ -ᵥ t₁ ⊆ s₂ -ᵥ t₂ :=
  image2_subset

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

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

Разделы

Аффилиация

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