mem_disjSum — Mathlib

English

Let s and t be multisets. For any x in α ⊕ β, x belongs to s.disjSum t iff x is of the form inl a with a ∈ s or of the form inr b with b ∈ t.

Русский

Пусть s и t — мультимножества. Для любого x ∈ α ⊕ β: x ∈ s.disjSum t тогда и только тогда, когда x имеет вид inl(a) с a ∈ s или inr(b) с b ∈ t.

LaTeX

$$$ x \\in s.disjSum t \\iff (\\exists a, a \\in s \\land inl a = x) \\lor \\exists b, b \\in t \\land inr b = x $$$

Lean4

theorem mem_disjSum : x ∈ s.disjSum t ↔ (∃ a, a ∈ s ∧ inl a = x) ∨ ∃ b, b ∈ t ∧ inr b = x := by
  simp_rw [disjSum, mem_add, mem_map]

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