English
Let γ: α → Type*, and s : ∀ i, γ i → Set β. Then ⋂ i, ⋂ a, s i a = ⋂ ia : Sigma γ, s ia.1 ia.2.
Русский
Пусть γ: α → Type*, и s: ∀ i, γ i → Set β. Тогда ⋂ i, ⋂ a, s i a = ⋂ ia : Sigma γ, s ia.1 ia.2.
LaTeX
$$$$\\bigcap_{i} \\bigcap_{a} s(i,a) = \\bigcap_{ia\\in \\Sigma\\gamma} s(ia.1, ia.2)$$$$
Lean4
theorem iInter_sigma' {γ : α → Type*} (s : ∀ i, γ i → Set β) : ⋂ i, ⋂ a, s i a = ⋂ ia : Sigma γ, s ia.1 ia.2 :=
iInf_sigma' _