mem_union — Mathlib

English

For any a and multisets s, t, we have a ∈ s ∪ t if and only if a ∈ s or a ∈ t.

Русский

Для любого элемента a и мультимножества s, t верно: a ∈ s ∪ t тогда и только тогда, когда a ∈ s или a ∈ t.

LaTeX

$$$a \\in s \\cup t \\;\\iff\\; a \\in s \\lor a \\in t$$$

Lean4

@[simp]
theorem mem_union : a ∈ s ∪ t ↔ a ∈ s ∨ a ∈ t :=
  ⟨fun h => (mem_add.1 h).imp_left (mem_of_le <| Multiset.sub_le_self _ _),
    (Or.elim · (mem_of_le le_union_left) (mem_of_le le_union_right))⟩

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