English
An element belongs to the closure of {a,b} iff it is a product a^m b^n for some natural m,n.
Русский
Элемент принадлежит замыканию {a,b} тогда и только тогда, когда он равен a^m b^n для некоторых натуральных m,n.
LaTeX
$$$ c \\in \\operatorname{closure}(\\{a,b\\}) \\iff \\exists m,n: \\mathbb{N}, a^m b^n = c $$$
Lean4
/-- An element is in the closure of a two-element set if it is a linear combination of those two
elements. -/
@[to_additive /-- An element is in the closure of a two-element set if it is a linear combination of
those two elements. -/
]
theorem mem_closure_pair {A : Type*} [CommMonoid A] (a b c : A) :
c ∈ Submonoid.closure ({ a, b } : Set A) ↔ ∃ m n : ℕ, a ^ m * b ^ n = c :=
by
rw [← Set.singleton_union, Submonoid.closure_union, mem_sup]
simp_rw [mem_closure_singleton, exists_exists_eq_and]
