not_disjoint_iff_nonempty_inter — Mathlib

English

Two finite sets s and t are not disjoint if and only if their intersection is nonempty.

Русский

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

LaTeX

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

Lean4

theorem not_disjoint_iff_nonempty_inter : ¬Disjoint s t ↔ (s ∩ t).Nonempty :=
  not_disjoint_iff.trans <| by simp [Finset.Nonempty]

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