English
Let α be a complete lattice and s: ι → α. Then the supremum of the family {s(i)} over i ∈ ι equals the supremum over all finite subfamilies: sup_i s(i) = sup_{T ⊆ ι, T finite} sup_{i ∈ T} s(i).
Русский
Пусть α — полная решетка и s: ι → α. Тогда верхняя грань семейства {s(i)} по i ∈ ι равна верхней грани по всем конечным подподсемействам: ⨆_{i ∈ ι} s(i) = ⨆_{T ⊆ ι, T конечна} ⨆_{i ∈ T} s(i).
LaTeX
$$$$\\displaystyle \\sup_{i \\in \\iota} s(i) = \\sup_{T \\subseteq \\iota,\\ T\\ \\text{finite}} \\left( \\sup_{i \\in T} s(i) \\right). $$$$
Lean4
/-- Supremum of `s i`, `i : ι`, is equal to the supremum over `t : Finset ι` of suprema
`⨆ i ∈ t, s i`. This version assumes `ι` is a `Type*`. See `iSup_eq_iSup_finset'` for a version
that works for `ι : Sort*`. -/
theorem iSup_eq_iSup_finset (s : ι → α) : ⨆ i, s i = ⨆ t : Finset ι, ⨆ i ∈ t, s i := by
classical
refine le_antisymm ?_ ?_
· exact iSup_le fun b => le_iSup_of_le { b } <| le_iSup_of_le b <| le_iSup_of_le (by simp) <| le_rfl
· exact iSup_le fun t => iSup_le fun b => iSup_le fun _ => le_iSup _ _
