English
Let s ⊆ ι, t: ∀ i, Set(α i), and f: ∀ i, α i → β. Then the iterated supremum over i ∈ s and j ∈ t i equals the supremum over ij ∈ s.sigma t of f(i,j).
Русский
Пусть s ⊆ ι, t: ∀ i, Set(α i), и f: ∀ i, α i → β. Тогда двойной верхний предел по i ∈ s и j ∈ t i равен верхнему пределу по всем ij ∈ s.sigma t от f(i,j).
LaTeX
$$$\bigsqcup_{i \in s} \bigsqcup_{j \in t(i)} f(i,j) = \bigsqcup_{(i,j) \in s \sigma t} f(i,j)$$$
Lean4
theorem _root_.biSup_sigma' (s : Set ι) (t : ∀ i, Set (α i)) (f : ∀ i, α i → β) :
⨆ (i ∈ s) (j ∈ t i), f i j = ⨆ ij ∈ s.sigma t, f ij.fst ij.snd :=
Eq.symm (biSup_sigma _ _ _)
