ite_inter_compl_self

Mathlib.Order.BooleanAlgebra.Set

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

English

The intersection of t.ite s s' with the complement of t equals s' ∩ tᶜ.

Русский

Пересечение t.ite s s' с комплементом t равно s' ∩ tᶜ.

LaTeX

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

Lean4

@[simp]
theorem ite_inter_compl_self (t s s' : Set α) : t.ite s s' ∩ tᶜ = s' ∩ tᶜ := by rw [← ite_compl, ite_inter_self]

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

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

Разделы

Аффилиация

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