English
A reversed version of iInter_psigma with a curried map: for s : ∀ i, γ i → Set β, we have ⋂ i, ⋂ a, s i a = ⋂ ia : PSigma γ, s ia.1 ia.2.
Русский
Перевернутая версия iInter_psigma c каррированной картой: для s : ∀ i, γ i → Set β имеем ⋂ i, ⋂ a, s i a = ⋂ ia : PSigma γ, s ia.1 ia.2.
LaTeX
$$$$\\bigcap_{i} \\bigcap_{a} s(i,a) = \\bigcap_{ia \\in \\mathrm{PSigma}\\,\\gamma} s(ia.1, ia.2).$$$$
Lean4
/-- A reversed version of `iInter_psigma` with a curried map. -/
theorem iInter_psigma' {γ : α → Type*} (s : ∀ i, γ i → Set β) : ⋂ i, ⋂ a, s i a = ⋂ ia : PSigma γ, s ia.1 ia.2 :=
iInf_psigma' _