inter_symmDiff_distrib_right — Mathlib

English

Symmetric difference distributes over intersection on the right: s ∆ t ∩ u = (s ∩ u) ∆ (t ∩ u).

Русский

Симметрическая разность распределяется через пересечение справа: s ∆ t ∩ u = (s ∩ u) ∆ (t ∩ u).

LaTeX

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

Lean4

theorem inter_symmDiff_distrib_right (s t u : Set α) : s ∆ t ∩ u = (s ∩ u) ∆ (t ∩ u) :=
  inf_symmDiff_distrib_right _ _ _

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