English
Special case of tprod_iSup_decode₂ for sets: product over unions decoded from β equals product over the index set.
Русский
Особый случай разложения произведения по объединениям для множеств: произведение по объединениям равно произведению по индексу β.
LaTeX
$$$\\prod' i, m(\\bigcup_{b\\in decode_2 \\beta i} s(b)) = \\prod' b, m(s(b))$$$
Lean4
/-- If a function is countably sub-multiplicative then it is sub-multiplicative on finite sets -/
@[to_additive /-- If a function is countably sub-additive then it is sub-additive on finite sets -/
]
theorem rel_iSup_prod [CompleteLattice α] (m : α → M) (m0 : m ⊥ = 1) (R : M → M → Prop)
(m_iSup : ∀ s : ℕ → α, R (m (⨆ i, s i)) (∏' i, m (s i))) (s : γ → α) (t : Finset γ) :
R (m (⨆ d ∈ t, s d)) (∏ d ∈ t, m (s d)) :=
by
rw [iSup_subtype', ← Finset.tprod_subtype]
exact rel_iSup_tprod m m0 R m_iSup _
