biInf_finsetSigma — Mathlib

English

Dual to BiSup, the double infimum over the sigma-structure equals the iterated infimum: the infimum over ij ∈ s.sigma t of f ij equals the infimum over i ∈ s and j ∈ t i of f ⟨i,j⟩.

Русский

Вдвойной инфимум над сигмой эквивалентен повторному применению инфимума по i, затем по j.

LaTeX

$$$$ \bigwedge_{ij \in s.sigma t} f(ij) = \bigwedge_{i \in s} \bigwedge_{j \in t(i)} f(\langle i,j \rangle) $$$$

Lean4

theorem _root_.biInf_finsetSigma [CompleteLattice β] (s : Finset ι) (t : ∀ i, Finset (α i)) (f : Sigma α → β) :
    ⨅ ij ∈ s.sigma t, f ij = ⨅ (i ∈ s) (j ∈ t i), f ⟨i, j⟩ :=
  biSup_finsetSigma (β := βᵒᵈ) _ _ _

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