mem_disjUnion — Mathlib

English

If s and t are disjoint, membership in the disjUnion s disjoint union t equals membership in s or membership in t.

Русский

Если s и t непересекаются, принадлежность элементу в disjUnion s t равна принадлежности элементу либо s, либо t.

LaTeX

$$$a \\in s.disjUnion t h \\iff a \\in s \\lor a \\in t$$$

Lean4

@[simp, grind =]
theorem mem_disjUnion {α s t h a} : a ∈ @disjUnion α s t h ↔ a ∈ s ∨ a ∈ t := by rcases s with ⟨⟨s⟩⟩;
  rcases t with ⟨⟨t⟩⟩; apply List.mem_append

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