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