disjointed_subset

Mathlib.Order.Disjointed

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

English

For every i, disjointed f i is a subset of f i.

Русский

Для каждого i дисконтированная последовательность disjointed f i является подмножеством f i.

LaTeX

$$$\forall i:\ ι,\; \operatorname{disjointed} f i \subseteq f i$$$

Lean4

theorem disjointed_subset [Preorder ι] [LocallyFiniteOrderBot ι] (f : ι → Set α) (i : ι) : disjointed f i ⊆ f i :=
  disjointed_le f i

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

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

Разделы

Аффилиация

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