not_disjoint_iff — Mathlib

English

¬Disjoint s t is equivalent to ∃ a, a ∈ s ∧ a ∈ t.

Русский

Не пересечение эквивалентно существованию элемента, принадлежащего обоим множествам.

LaTeX

$$$ \\lnot \\operatorname{Disjoint}(s,t) \\iff \\exists a, a \\in s \\land a \\in t $$$

Lean4

theorem not_disjoint_iff : ¬Disjoint s t ↔ ∃ a, a ∈ s ∧ a ∈ t :=
  disjoint_left.not.trans <| not_forall.trans <| exists_congr fun _ => by rw [Classical.not_imp, not_not]

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