diff_self_inter

Mathlib.Order.BooleanAlgebra.Set

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

English

Let S and T be sets. Then S \\ (S ∩ T) = S \\ T.

Русский

Пусть S и T — множества. Тогда S \\ (S ∩ T) = S \\ T.

LaTeX

$$$ S \\\\setminus (S \\\\cap T) = S \\\\setminus T $$$

Lean4

@[simp]
theorem diff_self_inter {s t : Set α} : s \ (s ∩ t) = s \ t :=
  sdiff_inf_self_left _ _

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

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

Разделы

Аффилиация

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