mem_closure_singleton — Mathlib

English

The closure of a singleton {x} in AddSubmonoid equals the image of the multiples Hom; i.e., it is the set of all natural multiples of x.

Русский

Замыкание одиночного элемента {x} в AddSubmonoid равно образу множителей Hom; то есть множество всех натуральных кратных x.

LaTeX

$$$ \\operatorname{closure}({x}) = \\mathrm{mrange}(\\text{multiplesHom } A\\ x) $$$

Lean4

/-- The `AddSubmonoid` generated by an element of an `AddMonoid` equals the set of
natural number multiples of the element. -/
theorem mem_closure_singleton {x y : A} : y ∈ closure ({ x } : Set A) ↔ ∃ n : ℕ, n • x = y := by
  rw [closure_singleton_eq, AddMonoidHom.mem_mrange]; rfl

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