mem_closure_range_iff — Mathlib

English

For a commutative group M, a family f: ι → M, and x ∈ closure(range f), there exists a finite-exponent expression x = ∏_{i ∈ ι} f(i)^{a(i)} with a(i) ∈ ℤ.

Русский

Пусть M — коммутативная группа, f: ι → M, и x ∈ closure(range f). Тогда существует выражение x = ∏ f(i)^{a(i)} с конечной опорой и a(i) ∈ ℤ.

LaTeX

$$$x \in \overline{\mathrm{range}(f)} \iff \exists a: ι \to \mathbb{Z},\; x = \prod_{i} f(i)^{a(i)}$$$

Lean4

@[to_additive]
theorem mem_closure_range_iff : x ∈ closure (Set.range f) ↔ ∃ a : ι →₀ ℤ, x = a.prod (f · ^ ·) :=
  by
  refine ⟨exists_finsupp_of_mem_closure_range f x, ?_⟩
  rintro ⟨a, rfl⟩
  exact Submonoid.prod_mem _ fun i hi ↦ zpow_mem (subset_closure (Set.mem_range_self i)) _

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