English
For a finite index set t and function f, if s is sup-closed and all f(i) ∈ s for i ∈ t, then the nested supremum over i ∈ t also lies in s.
Русский
Для конечного множества индексов t и функции f, если s_sup закрыто и все f(i) ∈ s, то объединение по i в t принадлежит s.
LaTeX
$$$\\text{Given } hs: \\operatorname{supClosed}(s),\\ ht: t.Finite,\\ ht': t.Nonempty,\\ hf: \\forall i\\in t, f(i)\\in s,\\text{ then } s \\ni iSup_{i \\in t} f(i).$$$
Lean4
theorem biSup_mem_of_nonempty {ι : Type*} {t : Set ι} {f : ι → α} (hs : SupClosed s) (ht : t.Finite) (ht' : t.Nonempty)
(hf : ∀ i ∈ t, f i ∈ s) : ⨆ i ∈ t, f i ∈ s := by
rw [← sSup_image]
exact hs.sSup_mem_of_nonempty (ht.image _) (by simpa) (by simpa)
