exists_mem_zpowers — Mathlib

English

For x ∈ G and p: G → Prop, (∃ g ∈ zpowers x, p g) is equivalent to (∃ m ∈ ℤ, p (x^m)).

Русский

Для x ∈ G и p: G → Prop, (∃ g ∈ zpowers x, p(g)) эквивалентно (∃ m ∈ ℤ, p(x^m)).

LaTeX

$$$(\exists g \in \operatorname{zpowers}(x), p g) \iff \exists m \in \mathbb Z, p(x^m)$$$

Lean4

@[to_additive]
theorem exists_mem_zpowers {x : G} {p : G → Prop} : (∃ g ∈ zpowers x, p g) ↔ ∃ m : ℤ, p (x ^ m) :=
  Set.exists_range_iff

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