mem_closure_range_iff_of_fintype — Mathlib

English

If ι is finite and f: ι → M, then x ∈ closure(range f) iff there exists a ∈ ι → ℤ with x = ∏_{i} f(i)^{a(i)}.

Русский

Пусть ι конечно, f: ι → M. Тогда x ∈ closure(range f) тогда и только тогда, когда существует a ∈ ι → ℤ с x = ∏ f(i)^{a(i)}.

LaTeX

$$$x \in \overline{\mathrm{range}(f)} \iff \exists a: ι \to \mathbb{Z},\; 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

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