mem_union_of_disjoint — Mathlib

English

For a disjoint pair s and t, for any x, x ∈ s ∪ t is equivalent to x ∈ s xor x ∈ t.

Русский

Для пары несовместных множеств s и t, для любого x, x ∈ s ∪ t эквивалентно (x ∈ s) xor (x ∈ t).

LaTeX

$$$(\forall x)(x \in s \cup t \iff (x \in s) \oplus (x \in t))$$$

Lean4

theorem mem_union_of_disjoint (h : Disjoint s t) {x : α} : x ∈ s ∪ t ↔ Xor' (x ∈ s) (x ∈ t) := by
  grind [Xor', Set.disjoint_left]

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