inter_union_compl

Mathlib.Order.BooleanAlgebra.Set

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

English

For sets s,t: s ∩ t ∪ s ∩ t^c = s.

Русский

Для множеств s,t: s ∩ t ∪ s ∩ t^c = s.

LaTeX

$$ (s ∩ t) ∪ (s ∩ t^{c}) = s$$

Lean4

@[simp]
theorem inter_union_compl (s t : Set α) : s ∩ t ∪ s ∩ tᶜ = s :=
  inter_union_diff _ _

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

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

Разделы

Аффилиация

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