vsub_self_mono

Mathlib.Algebra.Group.Pointwise.Set.Scalar

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

English

If s ⊆ t, then s −ᵥ s ⊆ t −ᵥ t.

Русский

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

LaTeX

$$$ s \subseteq t \Rightarrow s -ᵥ s \subseteq t -ᵥ t $$$

Lean4

theorem vsub_self_mono (h : s ⊆ t) : s -ᵥ s ⊆ t -ᵥ t :=
  vsub_subset_vsub h h

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

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

Разделы

Аффилиация

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