inter_sdiff_left_comm

Mathlib.Data.Finset.SDiff

URI: https://scilib.ai/kg/mathlib#Finset.inter_sdiff_left_comm

English

Intersection distributes over SDiff from the left: s ∩ (t \\ u) = t ∩ (s \\ u).

Русский

Пересечение слева распределяется над разностью: s ∩ (t \\ u) = t ∩ (s \\ u).

LaTeX

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

Lean4

theorem inter_sdiff_left_comm (s t u : Finset α) : s ∩ (t \ u) = t ∩ (s \ u) :=
  inf_sdiff_left_comm ..

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

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

Разделы

Аффилиация

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