mem_symmDiff — Mathlib

English

Characterization of membership in symmetric difference: a ∈ s ∆ t iff (a ∈ s ∧ a ∉ t) ∨ (a ∈ t ∧ a ∉ s).

Русский

Характеризация принадлежности симметрической разности: a ∈ s ∆ t эквивалентно (a ∈ s и a ∉ t) или (a ∈ t и a ∉ s).

LaTeX

$$$a \\in s \\Delta t \\iff (a \\in s \\wedge a \\notin t) \\lor (a \\in t \\wedge a \\notin s)$$$

Lean4

theorem mem_symmDiff : a ∈ s ∆ t ↔ a ∈ s ∧ a ∉ t ∨ a ∈ t ∧ a ∉ s :=
  Iff.rfl

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