English
For s ⊆ ι, t: ∀ i, Set(α i), and f: Σ i α i → β in a complete lattice β, the infimum over ij ∈ s.sigma t of f ij equals the infimum over i ∈ s and j ∈ t i of f ⟨i,j⟩.
Русский
Пусть s ⊆ ι, t: ∀ i, Set(α i), и f: Σ i α i → β в полной полудеже. Тогда наименьшая окрестность по всем парам (i,j) в s.sigma t равна по i ∈ s и j ∈ t i от f(⟨i,j⟩).
LaTeX
$$$\bigsqcap_{ij \in s.\sigma t} f(ij) = \bigsqcap_{i \in s} \bigsqcap_{j \in t(i)} f(\langle i,j\rangle)$$$
Lean4
theorem _root_.biInf_sigma (s : Set ι) (t : ∀ i, Set (α i)) (f : Sigma α → β) :
⨅ ij ∈ s.sigma t, f ij = ⨅ (i ∈ s) (j ∈ t i), f ⟨i, j⟩ :=
biSup_sigma (β := βᵒᵈ) _ _ _
