hasProd_of_prod_eq — Mathlib

English

Let f: β → α, g: γ → α be functions into a topological commutative monoid and suppose that for every finite subset U of γ there exists a finite subset V of β such that for every finite V' ⊇ V there is a finite U' ⊇ U with the equality of finite products ∏_{x∈U'} g(x) = ∏_{b∈V'} f(b). If HasProd g a holds, then HasProd f a also holds.

Русский

Пусть f: β → α, g: γ → α — функции в топологическом коммутативном моноиде. Пусть для каждого конечного множества U ⊆ γ существует конечное V ⊆ β такое, что для каждого V' ⊇ V существует U' ⊇ U с равенством конечных произведений ∏_{x∈U'} g(x) = ∏_{b∈V'} f(b). Если HasProd g a выполняется, то HasProd f a также выполняется.

LaTeX

$$$\forall U\Subset γ\,\exists V\Subset β\,\forall V'\supseteq V\,\exists U'\supseteq U\;:\; \prod_{x\in U'} g(x) = \prod_{b\in V'} f(b) \quad\Rightarrow\quad \text{HasProd } g a\;\Rightarrow\; \text{HasProd } f a$$$

Lean4

@[to_additive]
theorem hasProd_of_prod_eq {g : γ → α}
    (h_eq : ∀ u : Finset γ, ∃ v : Finset β, ∀ v', v ⊆ v' → ∃ u', u ⊆ u' ∧ ∏ x ∈ u', g x = ∏ b ∈ v', f b)
    (hf : HasProd g a) : HasProd f a :=
  le_trans (map_atTop_finset_prod_le_of_prod_eq h_eq) hf

Похожие утверждения