exists_lt_mem_inter_of_not_pairwiseDisjoint

English

Under a linear order on ι, if the family f: ι → Set α is not pairwise disjoint, there exist i < j and x ∈ f i ∩ f j.

Русский

При линейном порядке на ι, если семейство f: ι → Set α не попарно непересекается, существует i < j и x ∈ f i ∩ f j.

LaTeX

$$$$\text{If } \lnot (s.PAIRWISE_DISJOINT f) \text{ with } [\text{LinearOrder } ι], \exists i,j \in s, i < j \land \exists x \in f(i) \cap f(j).$$$$

Lean4

theorem exists_lt_mem_inter_of_not_pairwiseDisjoint [LinearOrder ι] {f : ι → Set α} (h : ¬s.PairwiseDisjoint f) :
    ∃ i ∈ s, ∃ j ∈ s, i < j ∧ ∃ x, x ∈ f i ∩ f j :=
  by
  obtain ⟨i, hi, j, hj, hne, x, hx₁, hx₂⟩ := exists_ne_mem_inter_of_not_pairwiseDisjoint h
  rcases lt_or_lt_iff_ne.mpr hne with h_lt | h_lt
  · exact ⟨i, hi, j, hj, h_lt, x, hx₁, hx₂⟩
  · exact ⟨j, hj, i, hi, h_lt, x, hx₂, hx₁⟩

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