English
Let ι' be a Sort and s: ι' → α with α a complete lattice. Then the supremum over i ∈ ι' of s(i) equals the supremum over finite sets t of PLift ι' of s(PLift.down i): ⨆ i, s(i) = ⨆ t : Finset (PLift ι'), ⨆ i ∈ t, s (PLift.down i).
Русский
Пусть ι' — сорт, a s: ι' → α, где α — полная решетка. Тогда верхняя граница по i ∈ ι' равна верхней границе по конечным подмножствам PLift ι' с соответствующим отображением: ⨆ i, s(i) = ⨆ t ∈ Finset(PLift ι'), ⨆ i ∈ t, s(PLift.down i).
LaTeX
$$$$\\displaystyle \\sup_{i \\in \\iota'} s(i) = \\sup_{t \\in \\mathrm{Finset}(\\mathrm{PLift} \\iota')} \\left( \\sup_{i \\in t} s(\\mathrm{PLift.down} i) \\right). $$$$
Lean4
/-- Supremum of `s i`, `i : ι`, is equal to the supremum over `t : Finset ι` of suprema
`⨆ i ∈ t, s i`. This version works for `ι : Sort*`. See `iSup_eq_iSup_finset` for a version
that assumes `ι : Type*` but has no `PLift`s. -/
theorem iSup_eq_iSup_finset' (s : ι' → α) : ⨆ i, s i = ⨆ t : Finset (PLift ι'), ⨆ i ∈ t, s (PLift.down i) := by
rw [← iSup_eq_iSup_finset, ← Equiv.plift.surjective.iSup_comp]; rfl
