English
Let f: β → α and g: γ → α be functions into a topological monoid. Suppose there are two finite-approximation conditions linking finite products of f and g in both directions. Then HasProd f a is equivalent to HasProd g a.
Русский
Пусть f: β → α и g: γ → α — функции в топологическом моноиде. Пусть существуют условия приближённости через конечные части, связывающие произведения конечных подмножеств для f и g в обе стороны. Тогда HasProd f a эквивалентно HasProd g a.
LaTeX
$$$\bigl(\forall U\Subset γ,\ \exists V\Subset β,\ \forall U'\Supseteq U,\ \exists V'\Supseteq V,\ \prod_{x\in U'} g(x)=\prod_{b\in V'} f(b)\bigr)\;\land\;\bigl(\forall V\Subset β,\ \exists U\Subset γ,\ \forall V'\Supseteq V,\ \exists U'\Supseteq U,\ \prod_{b\in V'} f(b)=\prod_{x\in U'} g(x)\bigr) \Rightarrow (\text{HasProd } f a \leftrightarrow \text{HasProd } g a)$$
Lean4
@[to_additive]
theorem hasProd_iff_hasProd {g : γ → α}
(h₁ : ∀ u : Finset γ, ∃ v : Finset β, ∀ v', v ⊆ v' → ∃ u', u ⊆ u' ∧ ∏ x ∈ u', g x = ∏ b ∈ v', f b)
(h₂ : ∀ v : Finset β, ∃ u : Finset γ, ∀ u', u ⊆ u' → ∃ v', v ⊆ v' ∧ ∏ b ∈ v', f b = ∏ x ∈ u', g x) :
HasProd f a ↔ HasProd g a :=
⟨HasProd.hasProd_of_prod_eq h₂, HasProd.hasProd_of_prod_eq h₁⟩
