biInter_sigma — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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