biInter_sigma' — Mathlib

English

Let s ⊆ ι, t: ∀ i, Set(α i), and f: ∀ i α i → Set β. Then the iterated intersection over i ∈ s and j ∈ t i equals the intersection over ij ∈ s.sigma t of f ij.fst ij.snd.

Русский

Пусть s ⊆ ι, t: ∀ i, Set(α i), и f: ∀ i α i → Set β. Тогда двойное пересечение по i ∈ s и j ∈ t i равно пересечению по ij ∈ s.sigma t от f ij.fst ij.snd.

LaTeX

$$$\bigcap_{i \in s} \bigcap_{j \in t(i)} f(i,j) = \bigcap_{(i,j) \in s\sigma t} f(i,j)$$$

Lean4

theorem biInter_sigma' (s : Set ι) (t : ∀ i, Set (α i)) (f : ∀ i, α i → Set β) :
    ⋂ i ∈ s, ⋂ j ∈ t i, f i j = ⋂ ij ∈ s.sigma t, f ij.fst ij.snd :=
  biInf_sigma' _ _ _

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