English
If a function is countably sub-multiplicative, then it is sub-multiplicative on countable index sets: the relation between iSup over a countable domain and the tprod of its evaluations holds.
Русский
Если функция подсчитывает по счётному индексу, то она сохраняет подумножение на счетном множестве индексов.
LaTeX
$$$\\forall m, \\, \\forall R, \\forall s:\\mathbb{N}\\to\\alpha,\\; R\\big(m(\\iSup_i s(i))\\,, \\prod_i m(s(i))\\big)$$$
Lean4
/-- If a function is countably sub-multiplicative then it is sub-multiplicative on countable
types -/
@[to_additive /-- If a function is countably sub-additive then it is sub-additive on countable types -/
]
theorem rel_iSup_tprod [CompleteLattice α] (m : α → M) (m0 : m ⊥ = 1) (R : M → M → Prop)
(m_iSup : ∀ s : ℕ → α, R (m (⨆ i, s i)) (∏' i, m (s i))) (s : β → α) : R (m (⨆ b : β, s b)) (∏' b : β, m (s b)) :=
by
cases nonempty_encodable β
rw [← iSup_decode₂, ← tprod_iSup_decode₂ _ m0 s]
exact m_iSup _
