diff_subset_diff_left

Mathlib.Order.BooleanAlgebra.Set

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

English

Let s1 ⊆ s2. Then s1 \ t ⊆ s2 \ t.

Русский

Пусть s1 ⊆ s2. Тогда s1 \ t ⊆ s2 \ t.

LaTeX

$$$s_1 \subseteq s_2 \Rightarrow s_1 \setminus t \subseteq s_2 \setminus t$$$

Lean4

theorem diff_subset_diff_left {s₁ s₂ t : Set α} (h : s₁ ⊆ s₂) : s₁ \ t ⊆ s₂ \ t :=
  sdiff_le_sdiff_right ‹s₁ ≤ s₂›

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

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

Разделы

Аффилиация

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