English
An induction principle for closure membership for predicates with two arguments: if a predicate p holds for all pairs coming from s and is preserved under multiplication in either coordinate, then p holds for all pairs in closure(s).
Русский
Принцип индукции по замыканию для предикатов с двумя аргументами: если p выполняется для всех пар из s и сохраняется при умножении по каждой координате, то p верно и для всех пар из closure(s).
LaTeX
$$$\\forall p:\\,(x,y) \\mapsto \\mathrm{Prop},\\ (\\forall x,y\\in s,\; p(x,y)) \\\\ \\land\\ (\\forall x,y,z,\\; p(x,z) \\to p(y,z) \\to p(xy,z)) \\\\ \\land\\ (\\forall x,y,z,\\; p(z,x) \\to p(z,y) \\to p(z,xy)) \\Rightarrow \\forall x,y \\in \\mathrm{closure}(s),\\; p(x,y)$$$
Lean4
@[to_additive]
theorem closure_singleton_le_iff_mem (m : M) (p : Subsemigroup M) : closure { m } ≤ p ↔ m ∈ p := by
rw [closure_le, singleton_subset_iff, SetLike.mem_coe]
