ite_diff_self

Mathlib.Order.BooleanAlgebra.Set

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

English

The difference of t.ite s s' from t equals s' .

Русский

Разность t.ite s s' и t равна s' \ t.

LaTeX

$$$$ (t.ite s s') \setminus t = s' \setminus t. $$$$

Lean4

@[simp]
theorem ite_diff_self (t s s' : Set α) : t.ite s s' \ t = s' \ t :=
  ite_inter_compl_self t s s'

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

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

Разделы

Аффилиация

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