closure_singleton_le_iff_mem — Mathlib

English

For a monoid M and a submonoid p of M, closure({m}) ≤ p if and only if m ∈ p.

Русский

Для моноида M и подмонома p верно: closure({m}) ≤ p тогда и только тогда, когда m ∈ p.

LaTeX

$$$\\operatorname{closure}({m}) \\le p \\quad\\Leftrightarrow\\quad m \\in p$$$

Lean4

@[to_additive]
theorem closure_singleton_le_iff_mem (m : M) (p : Submonoid M) : closure { m } ≤ p ↔ m ∈ p := by
  rw [closure_le, singleton_subset_iff, SetLike.mem_coe]

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