biInf_finsetSigma' — Mathlib

English

A prime variant of the double infimum over sigma; equivalently, the same dual equality with a different representation.

Русский

Прайм-вариант двойного инфимума над сигмой.

LaTeX

$$$$ \mathrm{i}\mathrm{Inf}_{\text{finset}}'\; = \; \mathrm{i}\mathrm{Inf}_{\text{finset}} $$$$

Lean4

theorem _root_.biInf_finsetSigma' [CompleteLattice β] (s : Finset ι) (t : ∀ i, Finset (α i)) (f : ∀ i, α i → β) :
    ⨅ (i ∈ s) (j ∈ t i), f i j = ⨅ ij ∈ s.sigma t, f ij.fst ij.snd :=
  Eq.symm (biInf_finsetSigma _ _ _)

Похожие утверждения