disjoint_or_nonempty_inter

Mathlib.Data.Set.Disjoint

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

English

Disjoint s t or (s ∩ t).Nonempty holds always.

Русский

Любые множества либоDisjoint, либо их пересечение непусто.

LaTeX

$$$\mathrm{Disjoint}(s,t) \lor (s \cap t).\mathrm{Nonempty}$$$

Lean4

theorem disjoint_or_nonempty_inter (s t : Set α) : Disjoint s t ∨ (s ∩ t).Nonempty :=
  (em _).imp_right not_disjoint_iff_nonempty_inter.1

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

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

Разделы

Аффилиация

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