mem_closure_range_iff_of_fintype — Mathlib

English

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

Русский

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

LaTeX

$$$[\text{Fintype } ι] \Rightarrow (x \in \overline{\mathrm{range}(f)}) \Leftrightarrow \exists a : ι \to \mathbb{N},\ x = \prod_i f_i^{a(i)}$$$

Lean4

@[to_additive]
theorem mem_closure_range_iff_of_fintype [Fintype ι] : x ∈ closure (Set.range f) ↔ ∃ a : ι → ℕ, x = ∏ i, f i ^ a i :=
  by
  rw [Finsupp.equivFunOnFinite.symm.exists_congr_left, mem_closure_range_iff]
  simp

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