inter_symmDiff_distrib_left

Mathlib.Data.Set.SymmDiff

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

English

s ∩ t ∆ u = (s ∩ t) ∆ (s ∩ u).

Русский

Перемещение симметрической разности через пересечение слева: s ∩ t ∆ u = (s ∩ t) ∆ (s ∩ u).

LaTeX

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

Lean4

theorem inter_symmDiff_distrib_left (s t u : Set α) : s ∩ t ∆ u = (s ∩ t) ∆ (s ∩ u) :=
  inf_symmDiff_distrib_left _ _ _

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

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

Разделы

Аффилиация

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