biInter_finsetSigma_univ — Mathlib

English

Similarly for intersections: the intersection over all (i,j) in s.sigma equals the iterated intersection over i ∈ s and j.

Русский

Аналогично для пересечений: пересечение по всем (i,j) в s.sigma равно поочередному пересечению по i в s и по j.

LaTeX

$$$\bigcap_{(i,j)\in s.\sigma} f(i,j) = \bigcap_{i\in s} \bigcap_j f(i,j)$$$

Lean4

theorem biInter_finsetSigma_univ (s : Finset ι) (f : Sigma κ → Set α) :
    ⋂ ij ∈ s.sigma fun _ ↦ Finset.univ, f ij = ⋂ i ∈ s, ⋂ j, f ⟨i, j⟩ := by aesop

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