sdiff_sdiff_eq_self

Mathlib.Data.Finset.SDiff

URI: https://scilib.ai/kg/mathlib#Finset.sdiff_sdiff_eq_self

English

If t ⊆ s, then s \ (s \ t) = t.

Русский

Если t ⊆ s, то s \ (s \ t) = t.

LaTeX

$$$ (t \subseteq s) \Rightarrow s \ (s \ t) = t $$$

Lean4

theorem sdiff_sdiff_eq_self (h : t ⊆ s) : s \ (s \ t) = t :=
  _root_.sdiff_sdiff_eq_self h

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

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

Разделы

Аффилиация

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