diff_diff_right_self

Mathlib.Order.BooleanAlgebra.Set

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

English

For any S, T, S \\\\ (S \\\\ T) = S ∩ T.

Русский

Для любых S, T: S \\\\ (S \\\\ T) = S ∩ T.

LaTeX

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

Lean4

theorem diff_diff_right_self (s t : Set α) : s \ (s \ t) = s ∩ t :=
  sdiff_sdiff_right_self

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

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

Разделы

Аффилиация

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