mem_disjUnion — Mathlib

English

Under the disjointness hypothesis, J belongs to π1.disjUnion π2 if and only if J belongs to π1 or J belongs to π2.

Русский

При условии несовместности J принадлежит π1.disjUnion π2 тогда и только тогда, когда J принадлежит π1 или π2.

LaTeX

$$$ J \in π_1.disjUnion π_2 H \iff J \in π_1 \lor J \in π_2. $$$

Lean4

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

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