English
Let s be a finite set of indices, t a function from indices to finite sets, and f a function into a complete lattice. Then the greatest lower bound of the values f on the union of all t(x) (as x ranges over s) equals the greatest lower bound obtained by first taking the infimum over each t(x) and then infimuming over x in s:
Русский
Пусть s — конечно заданное множество индексов, t — функция, сопоставляющая каждому индексу конечный множество, и f — функция в полную решетку. Тогда наименьшая верхняя граница значений f на объединении всех t(x) при x∈s равна наименьшей границе, полученной сначала по y∈t(x) для каждого x, затем по x∈s
LaTeX
$$$$\\inf_{y \\in \\bigcup_{x \\in s} t(x)} f(y) = \\inf_{x \\in s} \\inf_{y \\in t(x)} f(y)$$$$
Lean4
theorem iInf_biUnion (s : Finset γ) (t : γ → Finset α) (f : α → β) :
⨅ y ∈ s.biUnion t, f y = ⨅ (x ∈ s) (y ∈ t x), f y :=
@iSup_biUnion _ βᵒᵈ _ _ _ _ _ _
