Ici_iSup — Mathlib

English

For a family f(i,j) indexed by two indices, the set Ici of the two-parameter iSup equals the intersection over both indices of Ici(f(i,j)).

Русский

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

LaTeX

$$$$ \\operatorname{Ici}\\Big(\\big\\lvert\\!\\!\\big\\rVert_{i,j} f(i,j)\\big) = \\bigcap_i \\bigcap_j \\operatorname{Ici}(f(i,j)). $$$$

Lean4

theorem Ici_iSup (f : ι → α) : Ici (⨆ i, f i) = ⋂ i, Ici (f i) :=
  ext fun _ => by simp only [mem_Ici, iSup_le_iff, mem_iInter]

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