English
Dually to Sup Sigma, for a complete lattice with an order-top, the infimum over the sigma-construction equals the infimum over i ∈ s of the infimum over b ∈ t(i) of f(i,b).
Русский
Аналогично по отношению к inf, для полной решетки с верхней границей, InfSigma равен инфимуму по i ∈ s от инфимума по b ∈ t(i) от f(i,b).
LaTeX
$$$$ (s.\\sigma t).\\mathrm{inf}\, f = s.\\mathrm{inf}\\,\\bigl( i \\mapsto (t(i)).\\mathrm{inf}\\, (b \\mapsto f\\langle i,b\\rangle) \\bigr) $$$$
Lean4
theorem inf_sigma [SemilatticeInf β] [OrderTop β] : (s.sigma t).inf f = s.inf fun i => (t i).inf fun b => f ⟨i, b⟩ :=
@sup_sigma _ _ βᵒᵈ _ _ _ _ _
