eq_or_disjoint

Mathlib.Data.Set.Pairwise.Basic

URI: https://scilib.ai/kg/mathlib#Set.PairwiseDisjoint.eq_or_disjoint

← MathLib Explorer

English

For any i, j in s, either i = j or f i and f j are disjoint.

Русский

Для любых i, j в s либо i = j, либо f i и f j непересекаются.

LaTeX

$$hs : s.PairwiseDisjoint f ⟹ ∀ i j ∈ s, i = j ∨ Disjoint (f i) (f j)$$

Lean4

theorem eq_or_disjoint (h : s.PairwiseDisjoint f) {i j : ι} (hi : i ∈ s) (hj : j ∈ s) : i = j ∨ Disjoint (f i) (f j) :=
  by
  rw [or_iff_not_imp_right]
  exact h.elim hi hj

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

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

Разделы

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

Аффилиация

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