biInter_finsetSigma_univ' — Mathlib

English

The same equality as above with a different orientation, in the form of the equivalence of the two sides.

Русский

Та же равенство, но в ином формате, выражающее эквивалентность двух сторон пересечения.

LaTeX

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

Lean4

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

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