closure_singleton_eq — Mathlib

English

The closure of a two-element set {a,b} in a commutative monoid equals combinations a^m b^n with m,n ∈ ℕ. Equivalently, c is in closure({a,b}) iff there exist m,n with a^m b^n = c.

Русский

Замыкание пары {a,b} в коммутативном моноиде состоит из всех элементов вида a^m b^n, m,n ∈ ℕ; эквивалентно тому, что c принадлежит closure({a,b}) если существуют m,n такие что a^m b^n = c.

LaTeX

$$$ c \\in \\operatorname{closure}(\\{a,b\\}) \\iff \\exists m,n \\in \\mathbb{N},\\ a^m b^n = c $$$

Lean4

theorem closure_singleton_eq (x : A) : closure ({ x } : Set A) = AddMonoidHom.mrange (multiplesHom A x) :=
  closure_eq_of_le (Set.singleton_subset_iff.2 ⟨1, one_nsmul x⟩) fun _ ⟨_n, hn⟩ =>
    hn ▸ nsmul_mem (subset_closure <| Set.mem_singleton _) _

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