English
If the range of f is bounded above, then the supremum of the partialSups equals the supremum of f: ⨆ i, partialSups f i = ⨆ i, f i.
Русский
Если множество значений f ограничено сверху, то максимальное верхнее значение частичных верхушек равно верхнему значению самих значений: ⨆ i, partialSups f i = ⨆ i, f i.
LaTeX
$$$\text{BddAbove}(\operatorname{Set.range} f) \Rightarrow \bigvee_i (\partialSups f i) = \bigvee_i f i$$$
Lean4
@[simp]
theorem ciSup_partialSups_eq [ConditionallyCompleteLattice α] {f : ι → α} (h : BddAbove (Set.range f)) :
⨆ i, partialSups f i = ⨆ i, f i := by
by_cases hι : Nonempty ι
· refine (ciSup_le fun i ↦ ?_).antisymm (ciSup_mono ?_ <| le_partialSups f)
· simpa only [partialSups_eq_ciSup_Iic] using ciSup_le fun i ↦ le_ciSup h _
· rwa [bddAbove_range_partialSups]
· exact congr_arg _ (funext (not_nonempty_iff.mp hι).elim)
