iInter_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

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

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