exists_of_mem_closure_range — Mathlib

English

If x lies in the closure of the range of f, there exists a finsupp a with x = ∏ f_i^{a_i}.

Русский

Если x лежит в замыкании образа f, тогда существует a: ι → ℕ с x = ∏ f_i^{a_i}.

LaTeX

$$$\exists a : ι \to \mathbb{N},\ x = \prod_i 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⟩

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