sdiff_idem

Mathlib.Order.UpperLower.Closure

URI: https://scilib.ai/kg/mathlib#UpperSet.sdiff_idem

English

The operation sdiff is idempotent in the second argument: (s.sdiff t).sdiff t = s.sdiff t.

Русский

Операция sdiff идемпотентна по второму аргументу: (s.sdiff t).sdiff t = s.sdiff t.

LaTeX

$$$ (s.sdiff t).sdiff t = s.sdiff t $$$

Lean4

@[simp]
protected theorem sdiff_idem (s : UpperSet α) (t : Set α) : (s.sdiff t).sdiff t = s.sdiff t :=
  SetLike.coe_injective sdiff_idem

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

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

Разделы

Аффилиация

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