mem_closure_singleton — Mathlib

English

Let M be a monoid and x ∈ M. The submonoid generated by x consists exactly of the natural powers x^n (n ∈ ℕ). Equivalently, y ∈ closure({x}) if and only if y = x^n for some n ∈ ℕ.

Русский

Пусть M — моноид и x ∈ M. Подмоноид, порождаемый x, состоит ровно из степеней x: x^n (n ∈ ℕ). Эквивалентно: y ∈ closure({x}) тогда и только тогда, когда ∃ n ∈ ℕ, x^n = y.

LaTeX

$$$y \\\\in \\\\operatorname{closure}(\\\\{x\\\\}) \\\\iff \\\\exists n \\\\in \\\\mathbb{N}, x^n = y$$$

Lean4

/-- The submonoid generated by an element of a monoid equals the set of natural number powers of
the element. -/
theorem mem_closure_singleton {x y : M} : y ∈ closure ({ x } : Set M) ↔ ∃ n : ℕ, x ^ n = y := by
  rw [closure_singleton_eq, mem_mrange]; rfl

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