English
Without boundedness, in a ConditionallyCompleteLinearOrder, the same equality holds for the supremum of partialSups and f: ⨆ i, partialSups f i = ⨆ i, f i.
Русский
Без ограниченности, в линейном условно завершённом порядке та же равенство справедлива: ⨆ i, partialSups f i = ⨆ i, f i.
LaTeX
$$$[\text{ConditionallyCompleteLinearOrder }\alpha]\; (f: \iota \to \alpha) \;\Rightarrow \; ⨆ i, partialSups f i = ⨆ i, f i$$$
Lean4
/-- Version of `ciSup_partialSups_eq` without boundedness assumptions, but requiring a
`ConditionallyCompleteLinearOrder` rather than just a `ConditionallyCompleteLattice`. -/
@[simp]
theorem ciSup_partialSups_eq' [ConditionallyCompleteLinearOrder α] (f : ι → α) : ⨆ i, partialSups f i = ⨆ i, f i :=
by
by_cases h : BddAbove (Set.range f)
· exact ciSup_partialSups_eq h
·
rw [iSup, iSup, ConditionallyCompleteLinearOrder.csSup_of_not_bddAbove _ h,
ConditionallyCompleteLinearOrder.csSup_of_not_bddAbove _ (bddAbove_range_partialSups.not.mpr h)]
