closure_singleton_one — Mathlib

English

In any monoid, the submonoid generated by the identity 1 consists only of the identity, i.e., closure({1}) = ⊥.

Русский

В любом моноиде подмоноид, порождаемый единицей 1, состоит только из 1, то есть closure({1}) = ⊥.

LaTeX

$$$\\\\operatorname{closure}(\\\\{1\\\\}) = \\\\bot$$$

Lean4

theorem closure_singleton_one : closure ({ 1 } : Set M) = ⊥ := by simp [eq_bot_iff_forall, mem_closure_singleton]

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