biSup_finsetSigma' — Mathlib

English

A variant of the previous statement, swapping Sigma order, giving the same double supremum structure with a prime variant.

Русский

Вариант предыдущего утверждения с другой формулировкой двойного верхнего предела, обозначенный апострофом.

LaTeX

$$$$ \text{BiSup}_{\text{finset}}'\; = \; \text{BiSup}_{\text{finset}} $$$$

Lean4

theorem _root_.biSup_finsetSigma' [CompleteLattice β] (s : Finset ι) (t : ∀ i, Finset (α i)) (f : ∀ i, α i → β) :
    ⨆ (i ∈ s) (j ∈ t i), f i j = ⨆ ij ∈ s.sigma t, f ij.fst ij.snd :=
  Eq.symm (biSup_finsetSigma _ _ _)

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