disjoint_disjointed

Mathlib.Order.Disjointed

URI: https://scilib.ai/kg/mathlib#disjoint_disjointed

English

For any f, the family (disjointed f)(i) is pairwise disjoint as i ranges.

Русский

Для любого f множество (disjointed f)(i) попарно несовместимо по всем i.

LaTeX

$$$\forall f:\,\mathrm{Pairwise}(\mathrm{Disjoint}\; on\; \operatorname{disjointed} f).$$$

Lean4

theorem disjoint_disjointed (f : ι → α) : Pairwise (Disjoint on disjointed f) :=
  (pairwise_disjoint_on _).mpr fun _ _ ↦ disjoint_disjointed_of_lt f

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

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

Разделы

Аффилиация

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