not_disjoint_iff

Mathlib.Data.Set.Disjoint

URI: https://scilib.ai/kg/mathlib#Set.not_disjoint_iff

English

¬Disjoint s t iff ∃ x, x ∈ s ∧ x ∈ t.

Русский

Не дисjointность s и t эквивалентна существованию элемента x, принадлежащего и s, и t.

LaTeX

$$$\neg \mathrm{Disjoint}(s,t) \iff \exists x, x \in s \land x \in t$$$

Lean4

theorem not_disjoint_iff : ¬Disjoint s t ↔ ∃ x, x ∈ s ∧ x ∈ t :=
  Set.disjoint_iff.not.trans <| not_forall.trans <| exists_congr fun _ ↦ not_not

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru