mem_join — Mathlib

English

An element a belongs to the join of a collection of multisets S if and only if a belongs to some member of S.

Русский

Элемент a принадлежит объединению join S тогда и только тогда, когда он принадлежит некоторому элементу S.

LaTeX

$$$a \\in \\operatorname{join}(S) \\iff \\exists s \\in S, a \\in s$$$

Lean4

@[simp]
theorem mem_join {a S} : a ∈ @join α S ↔ ∃ s ∈ S, a ∈ s :=
  Multiset.induction_on S (by simp) <| by simp +contextual [or_and_right, exists_or]

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