mem_closure_range_iff — Mathlib

English

If ι is finite, then x ∈ closure(range f) iff there exists a: ι → ℕ with x = ∏_i f_i^{a_i}.

Русский

Пусть ι конечно; тогда x ∈ closure(range f) эквивалентно существованию a: ι → ℕ с x = ∏ f_i^{a_i}.

LaTeX

$$$[\text{Fintype } \iota] \Rightarrow (x \in \overline{\mathrm{range}(f)}) \Leftrightarrow \exists a : \iota \to \mathbb{N},\ 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 prod_mem _ fun i hi ↦ pow_mem (subset_closure (Set.mem_range_self i)) _

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