iInter_psigma' — Mathlib

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' _

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