pairwiseDisjoint_slice

Mathlib.Data.Finset.Slice

URI: https://scilib.ai/kg/mathlib#Finset.pairwiseDisjoint_slice

← MathLib Explorer

English

The family {𝒜_r} across r ∈ Set.univ is pairwise disjoint.

Русский

Семейство {𝒜_r} по всем r из Set.univ попарно непересекается.

LaTeX

$$$ (Set.univ : Set \mathbb{N}).\PairwiseDisjoint (\mathcal{A}_r) $$$

Lean4

theorem pairwiseDisjoint_slice : (Set.univ : Set ℕ).PairwiseDisjoint (slice 𝒜) := fun _ _ _ _ hmn =>
  disjoint_filter.2 fun _s _hs hm hn => hmn <| hm.symm.trans hn

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

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

Разделы

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

Аффилиация

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