English
Let α be a complete lattice and M a commutative monoid. Suppose a function m: α → M with m(⊥) = 1 satisfies a relation R between m of countable suprema and the infinite product of its values: for every sequence s: ℕ → α, R(m(⨆ i, s i), ∏' i, m(s i)). Then for any s1, s2 ∈ α one has R(m(s1 ⊔ s2), m(s1) m(s2)).
Русский
Пусть α — полная решетка, M — коммутативный моноид. Пусть функция m: α → M удовлетворяет условию, что m(⊥) = 1 и для любой последовательности s: ℕ → α выполняется отношение R между m(⨆ i, s i) и бесконечным произведением ∏′ i, m(s i). Тогда для любых s1, s2 ∈ α справедливо R(m(s1 ⊔ s2), m(s1) m(s2)).
LaTeX
$$$R\bigl(m(s_1 \vee s_2),\ m(s_1) \cdot m(s_2)\bigr)$$$
Lean4
/-- If a function is countably sub-multiplicative then it is binary sub-multiplicative -/
@[to_additive /-- If a function is countably sub-additive then it is binary sub-additive -/
]
theorem rel_sup_mul [CompleteLattice α] (m : α → M) (m0 : m ⊥ = 1) (R : M → M → Prop)
(m_iSup : ∀ s : ℕ → α, R (m (⨆ i, s i)) (∏' i, m (s i))) (s₁ s₂ : α) : R (m (s₁ ⊔ s₂)) (m s₁ * m s₂) :=
by
convert rel_iSup_tprod m m0 R m_iSup fun b ↦ cond b s₁ s₂
· simp only [iSup_bool_eq, cond]
· rw [tprod_fintype, Fintype.prod_bool, cond, cond]
