ite_same

Mathlib.Order.BooleanAlgebra.Set

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

English

The ITE operator with identical middle arguments returns the middle argument: t.ite s s = s.

Русский

Оператор ITE с одинаковыми вторыми аргументами возвращает второй аргумент: t.ite s s = s.

LaTeX

$$$$ t.ite s s = s. $$$$

Lean4

@[simp]
theorem ite_same (t s : Set α) : t.ite s s = s :=
  inter_union_diff _ _

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

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

Разделы

Аффилиация

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