univ_disjoint

Mathlib.Data.Set.Disjoint

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

English

Let s be a subset of α. Then Disjoint(s, univ) holds if and only if s is empty.

Русский

Пусть s ⊆ α. Тогда Disjoint(s, univ) выполняется тогда и только тогда, когда s пусто.

LaTeX

$$$Disjoint(s, \mathrm{univ}) \iff s = \emptyset$$$

Lean4

@[simp]
theorem univ_disjoint : Disjoint univ s ↔ s = ∅ :=
  top_disjoint

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

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

Разделы

Аффилиация

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