intersecting_singleton

Mathlib.Combinatorics.SetFamily.Intersecting

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

English

A singleton set {a} is intersecting iff a ≠ ⊥.

Русский

Множество вида {a} пересекается тогда и только тогда, когда a ≠ ⊥.

LaTeX

$$$$\\{a\\} \\text{ is intersecting} \\iff a \\neq \\bot$$$$

Lean4

@[simp]
theorem intersecting_singleton : ({ a } : Set α).Intersecting ↔ a ≠ ⊥ := by simp [Intersecting]

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

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

Разделы

Аффилиация

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