iInter₂_comm — Mathlib

English

For s : ∀ i, κ i → ∀ i', κ' i' → Set α, the fourfold intersection is symmetric in the two index sectors: ⋂ i (j) (i') (j'), s i j i' j' = ⋂ (i') (j') (i) (j), s i j i' j'.

Русский

Для s: ∀ i, κ i → ∀ i', κ' i' → Set α, пересечение по четырём индексам симметрично в двух частях индексов.

LaTeX

$$$$\\bigcap_{i} \\bigcap_{j} \\bigcap_{i'} \\bigcap_{j'} s(i,j,i',j') = \\bigcap_{i'} \\bigcap_{j'} \\bigcap_{i} \\bigcap_{j} s(i,j,i',j')$$$$

Lean4

theorem iInter₂_comm (s : ∀ i, κ i → ∀ i', κ' i' → Set α) :
    ⋂ (i) (j) (i') (j'), s i j i' j' = ⋂ (i') (j') (i) (j), s i j i' j' :=
  iInf₂_comm _

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