iSup_disjointed — Mathlib

English

The supremum over i of disjointed f i equals the supremum over i of f i:

Русский

Нормальный верхний предел по индексу i от disjointed f i равен верхнему пределу f i.

LaTeX

$$$\operatorname{iSup}_i\, \operatorname{disjointed} f i = \operatorname{iSup}_i f i$$$

Lean4

theorem iSup_disjointed [PartialOrder ι] [LocallyFiniteOrderBot ι] (f : ι → α) : ⨆ i, disjointed f i = ⨆ i, f i :=
  iSup_eq_iSup_of_partialSups_eq_partialSups (partialSups_disjointed f)

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