iUnion_psigma' — Mathlib

English

A reversed version of iUnion_psigma with a curried map: for s: ∀ i, γ i → Set β, we have ⋃ i, ⋃ a, s i a = ⋃ ia : PSigma γ, s ia.1 ia.2.

Русский

Перевернутая версия iUnion_psigma c каррированной картой: для s: ∀ i, γ i → Set β имеем ⋃ i, ⋃ a, s i a = ⋃ ia : PSigma γ, s ia.1 ia.2.

LaTeX

$$$$\\bigcup_{i} \\bigcup_{a} s(i,a) = \\bigcup_{ia \\in \\mathrm{PSigma}\\,\\gamma} s(ia.1, ia.2).$$$$

Lean4

/-- A reversed version of `iUnion_psigma` with a curried map. -/
theorem iUnion_psigma' {γ : α → Type*} (s : ∀ i, γ i → Set β) : ⋃ i, ⋃ a, s i a = ⋃ ia : PSigma γ, s ia.1 ia.2 :=
  iSup_psigma' _

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