English
In WithTop, the supremum of the coerced values equals top iff the index range is unbounded; equivalently, iSup (f) is top exactly when range f is not bounded above.
Русский
В WithTop, супремум приведенных значений равен верхнему элементу тогда и только тогда, когда диапазон значений не ограничен сверху.
LaTeX
$$$\\big\\vee_{x} (f(x)\\colon\\mathrm{WithTop}\\,\\alpha) = \\top \\iff \\lnot \\operatorname{BddAbove}(\\mathrm{range}\,f)$$$
Lean4
theorem iSup_coe_eq_top : ⨆ x, (f x : WithTop α) = ⊤ ↔ ¬BddAbove (range f) :=
by
rw [iSup_eq_top, not_bddAbove_iff]
refine ⟨fun hf r => ?_, fun hf a ha => ?_⟩
· rcases hf r (WithTop.coe_lt_top r) with ⟨i, hi⟩
exact ⟨f i, ⟨i, rfl⟩, WithTop.coe_lt_coe.mp hi⟩
· rcases hf (a.untop ha.ne) with ⟨-, ⟨i, rfl⟩, hi⟩
exact ⟨i, by simpa only [WithTop.coe_untop _ ha.ne] using WithTop.coe_lt_coe.mpr hi⟩
