exists_of_mem_closure_range — Mathlib

English

If x is in the closure of the range of f: ι → M with ι finite, there exists a finite-exponent expression x = ∏_{i ∈ ι} f(i)^{a(i)} with a(i) ∈ ℤ.

Русский

Если x лежит в замыкании образа f: ι → M при конечном ι, то существует выражение с конечными степенями: x = ∏ f(i)^{a(i)} с a(i) ∈ ℤ.

LaTeX

$$$|ι| < \infty \Rightarrow \exists a: ι \to \mathbb{Z}, x = \prod_{i \in ι} f(i)^{a(i)}$$$

Lean4

@[to_additive]
theorem exists_of_mem_closure_range [Fintype ι] (hx : x ∈ closure (Set.range f)) : ∃ a : ι → ℤ, x = ∏ i, f i ^ a i :=
  by
  obtain ⟨a, rfl⟩ := exists_finsupp_of_mem_closure_range f x hx
  exact ⟨a, by simp⟩

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