iUnion_sigma' — Mathlib

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

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

Lean4

theorem iUnion_sigma' {γ : α → Type*} (s : ∀ i, γ i → Set β) : ⋃ i, ⋃ a, s i a = ⋃ ia : Sigma γ, s ia.1 ia.2 :=
  iSup_sigma' _

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