elim_finset — Mathlib

English

If s is a set of indices with pairwise disjoint f, then if i, j ∈ s and a ∈ f(i) ∩ f(j), we must have i = j.

Русский

Если множество индексов s образует парно непересекающиеся f, то при i, j ∈ s и a ∈ f(i) ∩ f(j) должно выполняться i = j.

LaTeX

$$hs.elim hi hj a hai haj : i = j$$

Lean4

theorem elim_finset {s : Set ι} {f : ι → Finset α} (hs : s.PairwiseDisjoint f) {i j : ι} (hi : i ∈ s) (hj : j ∈ s)
    (a : α) (hai : a ∈ f i) (haj : a ∈ f j) : i = j :=
  hs.elim hi hj (Finset.not_disjoint_iff.2 ⟨a, hai, haj⟩)

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