Iic_iInf₂ — Mathlib

English

For a two-parameter family f(i,j), the higher-level Ici distributes over two iSup's into a double intersection of Ici's.

Русский

Для двойного семейства f(i,j) Ici(⨆i⨆j f(i,j)) представляет собой двойное пересечение Ici(f(i,j)).

LaTeX

$$$$ \\text{Ici}\\Big(\\big(\\sup_i \\sup_j f(i,j)\\big)\\Big) = \\bigcap_i \\bigcap_j \\mathrm{Ici}(f(i,j)). $$$$

Lean4

theorem Iic_iInf₂ (f : ∀ i, κ i → α) : Iic (⨅ (i) (j), f i j) = ⋂ (i) (j), Iic (f i j) := by simp_rw [Iic_iInf]

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