exists_ne_mem_inter_of_not_pairwise_disjoint

English

For any f: ι → Set α, if not pairwise disjoint then there exist i ≠ j with x ∈ f i ∩ f j.

Русский

Для любого f: ι → Set α, если не попарно непересекается, то найдутся i ≠ j и x ∈ f i ∩ f j.

LaTeX

$$$$\exists i,j, i \neq j \land \exists x, x \in f(i) \cap f(j).$$$$

Lean4

theorem exists_ne_mem_inter_of_not_pairwise_disjoint {f : ι → Set α} (h : ¬Pairwise (Disjoint on f)) :
    ∃ i j : ι, i ≠ j ∧ ∃ x, x ∈ f i ∩ f j := by
  rw [← pairwise_univ] at h
  obtain ⟨i, _hi, j, _hj, h⟩ := exists_ne_mem_inter_of_not_pairwiseDisjoint h
  exact ⟨i, j, h⟩

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