English
If a family f: ι → Set α is not pairwise disjoint, there exist i ≠ j in the index set and an element x that belongs to both f i and f j.
Русский
Если семейство f: ι → Set α не попарно непересекается, то существуют i ≠ j и элемент x, принадлежащий одновременно f i и f j.
LaTeX
$$$$\text{If } \lnot (s.PAIRWISE_DISJOINT f), \exists i \in s, \exists j \in s, i \neq j \land \exists x \in f(i) \cap f(j).$$$$
Lean4
theorem exists_ne_mem_inter_of_not_pairwiseDisjoint {f : ι → Set α} (h : ¬s.PairwiseDisjoint f) :
∃ i ∈ s, ∃ j ∈ s, i ≠ j ∧ ∃ x : α, x ∈ f i ∩ f j :=
by
change ¬∀ i, i ∈ s → ∀ j, j ∈ s → i ≠ j → ∀ t, t ≤ f i → t ≤ f j → t ≤ ⊥ at h
simp only [not_forall] at h
obtain ⟨i, hi, j, hj, h_ne, t, hfi, hfj, ht⟩ := h
replace ht : t.Nonempty := by rwa [le_bot_iff, bot_eq_empty, ← Ne, ← nonempty_iff_ne_empty] at ht
obtain ⟨x, hx⟩ := ht
exact ⟨i, hi, j, hj, h_ne, x, hfi hx, hfj hx⟩
