disjoint_or_nonempty_inter — Mathlib

English

For any finite sets s and t, either s and t are disjoint or their intersection is nonempty.

Русский

Для любых конечных множеств s и t либо они непересекаются, либо их пересечение непусто.

LaTeX

$$$$ \text{Disjoint}(S,T) \;\lor\; (S \cap T) \neq \emptyset, $$$$

Lean4

theorem disjoint_or_nonempty_inter (s t : Finset α) : Disjoint s t ∨ (s ∩ t).Nonempty :=
  by
  rw [← not_disjoint_iff_nonempty_inter]
  exact em _

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