elim_set — Mathlib

English

If a family f over s is pairwise disjoint in the sense of Set.PairwiseDisjoint f, and a ∈ f i and a ∈ f j for i,j ∈ s, then i = j.

Русский

Если семейство f над s попарно непересекается, и элемент a принадлежит одновременно f i и f j для i,j ∈ s, тогда i = j.

LaTeX

$$$$\text{If } hs : s.PAIRWISE_DISJOINT f, \ i,j \in s, a\in f(i), a\in f(j) \Rightarrow i=j.$$$$

Lean4

theorem elim_set {s : Set ι} {f : ι → Set α} (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 <| not_disjoint_iff.2 ⟨a, hai, haj⟩

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