forall_zpowers — Mathlib

English

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

Русский

Пусть x ∈ G и p: zpowers x → Prop. Тогда (∀ g ∈ zpowers x, p(g)) эквивалентно (∀ m ∈ ℤ, p(x^m)).

LaTeX

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

Lean4

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

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