mem_disjSum — Mathlib

English

An element x of α ⊕ β belongs to s.disjSum t if and only if x is of the form inl a with a ∈ s, or x is inr b with b ∈ t.

Русский

Элемент x ∈ α ⊕ β принадлежит s.disjSum t тогда и только тогда, когда x имеет вид inl(a) с a ∈ s, или x имеет вид inr(b) с b ∈ t.

LaTeX

$$$x \in s\disjSum t \iff (\exists a \in s, \mathrm{inl}(a) = x) \lor (\exists b \in t, \mathrm{inr}(b) = x)$$$

Lean4

theorem mem_disjSum : x ∈ s.disjSum t ↔ (∃ a, a ∈ s ∧ inl a = x) ∨ ∃ b, b ∈ t ∧ inr b = x :=
  Multiset.mem_disjSum

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