diff_subset_diff_right

Mathlib.Order.BooleanAlgebra.Set

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

English

Let t ⊆ u. Then s \ u ⊆ s \ t.

Русский

Пусть t ⊆ u. Тогда s \ u ⊆ s \ t.

LaTeX

$$$t \subseteq u \Rightarrow s \\setminus u \subseteq s \\setminus t$$$

Lean4

theorem diff_subset_diff_right {s t u : Set α} (h : t ⊆ u) : s \ u ⊆ s \ t :=
  sdiff_le_sdiff_left ‹t ≤ u›

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

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

Разделы

Аффилиация

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