mem_disjUnion — Mathlib

English

An element J belongs to the disjoint union if and only if it belongs to either π1 or π2.

Русский

Элемент J принадлежит дизъюнкции, если и только если он принадлежит либо π1, либо π2.

LaTeX

$$$ J ∈ π_1.disjUnion π_2 h \iff J ∈ π_1 ∨ J ∈ π_2 $$$

Lean4

@[simp]
theorem mem_disjUnion (h : Disjoint π₁.iUnion π₂.iUnion) : J ∈ π₁.disjUnion π₂ h ↔ J ∈ π₁ ∨ J ∈ π₂ := by
  classical exact Finset.mem_union

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