covering_disjoint

Mathlib.MeasureTheory.Covering.VitaliFamily

URI: https://scilib.ai/kg/mathlib#VitaliFamily.FineSubfamilyOn.covering_disjoint

English

The collection of the second components {p.2 : p ∈ h.index} is pairwise disjoint.

Русский

Множество вторых компонент {p.2 : p ∈ h.index} попарно несовпадающих.

LaTeX

$$$h.index\\text{.PairwiseDisjoint}(h.covering)$.$$

Lean4

theorem covering_disjoint : h.index.PairwiseDisjoint h.covering :=
  h.exists_disjoint_covering_ae.choose_spec.2.1

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

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

Разделы

Аффилиация

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