diff_inter

Mathlib.Order.BooleanAlgebra.Set

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

English

For sets s,t,u, s \ (t ∩ u) = (s \ t) ∪ (s \ u).

Русский

Для множеств S,T,U: S \ (T ∩ U) = (S \ T) ∪ (S \ U).

LaTeX

$$$s \\ (t \cap u) = (s \\ t) \\ (s \\ u)$$$$

Lean4

theorem diff_inter {s t u : Set α} : s \ (t ∩ u) = s \ t ∪ s \ u :=
  sdiff_inf

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

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

Разделы

Аффилиация

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