English
A product over a type β can be computed by taking a supremum over a decoding function and then multiplying over natural indices; this rewrites a product over encoded β into a product over β.
Русский
Произведение по β может выразиться через наивысшее объединение (iSup) после раскодирования и перемножения по натуральному индексу.
LaTeX
$$$\\prod' i:\\mathbb{N}, m(\\lceil \\!\\!\\rceil) = \\prod' b:\\beta, m(s(b))$$$
Lean4
/-- `tprod_iSup_decode₂` specialized to the complete lattice of sets. -/
@[to_additive /-- `tsum_iSup_decode₂` specialized to the complete lattice of sets. -/
]
theorem tprod_iUnion_decode₂ (m : Set α → M) (m0 : m ∅ = 1) (s : β → Set α) :
∏' i, m (⋃ b ∈ decode₂ β i, s b) = ∏' b, m (s b) :=
tprod_iSup_decode₂ m m0 s
