vsub_subset_vsub

Mathlib.Algebra.Group.Pointwise.Finset.Scalar

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

English

If s1 ⊆ s2, then 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

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

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

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

Разделы

Аффилиация

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