exists_zpowers — Mathlib

English

There exists g ∈ zpowers x such that p g iff there exists m ∈ ℤ with p ⟨x^m, m, rfl⟩.

Русский

Существует g ∈ zpowers(x) such that p(g) тогда и только если существует m ∈ ℤ с p(⟨x^m, m, rfl⟩).

LaTeX

$$$(\exists g, p g) \iff (\exists m \in \mathbb Z, p(\langle x^m, m, rfl\rangle))$$$

Lean4

@[to_additive (attr := simp 1100)]
theorem exists_zpowers {x : G} {p : zpowers x → Prop} : (∃ g, p g) ↔ ∃ m : ℤ, p ⟨x ^ m, m, rfl⟩ :=
  Set.exists_subtype_range_iff

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