ite_compl

Mathlib.Order.BooleanAlgebra.Set

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

English

Complementing the first argument of ITE swaps the last two arguments: tᶜ.ite s s' = t.ite s' s.

Русский

Дополнение первого аргумента ITE меняет местами второй и третий аргументы: t^c.ite s s' = t.ite s' s.

LaTeX

$$$$ (t^{c}.ite(s, s')) = t.ite(s', s). $$$$

Lean4

@[simp]
theorem ite_compl (t s s' : Set α) : tᶜ.ite s s' = t.ite s' s := by
  rw [Set.ite, Set.ite, diff_compl, union_comm, diff_eq]

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

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

Разделы

Аффилиация

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