denseRange_zpow_iff_pow — Mathlib

English

For any x ∈ G, DenseRange (x^· : ℤ → G) is equivalent to DenseRange (x^· : ℕ → G).

Русский

Для любого x ∈ G плотность диапазона функций x^· по целым числам эквивалентна плотности диапазона по натуральным числам.

LaTeX

$$$\operatorname{DenseRange}(x^{\cdot} : \mathbb{Z} \to G) \iff \operatorname{DenseRange}(x^{\cdot} : \mathbb{N} \to G).$$$

Lean4

@[to_additive]
theorem denseRange_zpow_iff_pow {x : G} : DenseRange (x ^ · : ℤ → G) ↔ DenseRange (x ^ · : ℕ → G) := by
  simp only [DenseRange, dense_iff_closure_eq, closure_range_zpow_eq_pow]

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