exists_finsupp_of_mem_closure_range

English

If x lies in the closure of the range of a family f: ι → M, then there exists a finitely supported function a: ι → ℕ such that x equals the product ∏_i f_i^{a_i}.

Русский

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

LaTeX

$$$\exists a : ι \to \mathbb{N},\ x = \prod_i (f_i)^{a(i)}$$$

Lean4

@[to_additive]
theorem exists_finsupp_of_mem_closure_range (hx : x ∈ closure (Set.range f)) : ∃ a : ι →₀ ℕ, x = a.prod (f · ^ ·) := by
  classical
    induction hx using closure_induction with
  | mem x h => obtain ⟨i, rfl⟩ := h; exact ⟨Finsupp.single i 1, by simp⟩
  | one => use 0; simp
  | mul x y hx hy hx' hy' =>
    obtain ⟨⟨v, rfl⟩, w, rfl⟩ := And.intro hx' hy'
    use v + w
    rw [Finsupp.prod_add_index]
    · simp
    · simp [pow_add]

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