mem_symmDiff — Mathlib

English

A helper for symmetric difference membership: a ∈ s ∆ t if and only if a belongs to exactly one of s or t.

Русский

Помощь по членству в симметрической разности: a принадлежит ровно одному из s или t.

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 := by
  simp_rw [symmDiff, sup_eq_union, mem_union, mem_sdiff]

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