English
Let α be a complete lattice and s: ι' → α. Then the infimum over i ∈ ι' of s(i) equals the infimum over Finset (PLift ι') of the infimum over i ∈ t of s (PLift.down i): ⨅ i, s i = ⨅ t : Finset (PLift ι'), ⨅ i ∈ t, s (PLift.down i).
Русский
Пусть α — полная решетка и s: ι' → α. Тогда инфиминум по i ∈ ι' от s(i) равен инфиминуму по Finset(PLift ι') от инфиминума по i ∈ t от s(PLift.down i).
LaTeX
$$$$\\displaystyle \\inf_{i \\in \\iota'} s(i) = \\inf_{t \\in \\mathrm{Finset}(\\mathrm{PLift} \\iota')} \\inf_{i \\in t} s(\\mathrm{PLift.down} i). $$$$
Lean4
/-- Infimum of `s i`, `i : ι`, is equal to the infimum over `t : Finset ι` of infima
`⨅ i ∈ t, s i`. This version works for `ι : Sort*`. See `iInf_eq_iInf_finset` for a version
that assumes `ι : Type*` but has no `PLift`s. -/
theorem iInf_eq_iInf_finset' (s : ι' → α) : ⨅ i, s i = ⨅ t : Finset (PLift ι'), ⨅ i ∈ t, s (PLift.down i) :=
@iSup_eq_iSup_finset' αᵒᵈ _ _ _
