diff_inter_self_eq_diff

Mathlib.Order.BooleanAlgebra.Set

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

English

For sets s,t, s \ (t ∩ s) = s \ t.

Русский

Для множеств S,T: S \ (T ∩ S) = S \ T.

LaTeX

$$$s \\ (t \cap s) = s \\ t$$$

Lean4

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

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

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

Разделы

Аффилиация

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