pairwiseDisjoint

Mathlib.Order.SupIndep

URI: https://scilib.ai/kg/mathlib#sSupIndep.pairwiseDisjoint

← MathLib Explorer

English

For distinct a,b, sSupIndep {a,b} holds iff Disjoint a b.

Русский

Для различных a,b, sSupIndep {a,b} эквивалентно Disjoint a b.

LaTeX

$$sSupIndep {a,b} ↔ Disjoint a b$$

Lean4

/-- If the elements of a set are independent, then any pair within that set is disjoint. -/
theorem pairwiseDisjoint : s.PairwiseDisjoint id := fun _ hx y hy h =>
  disjoint_sSup_right (hs hx) ((mem_diff y).mpr ⟨hy, h.symm⟩)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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