closure_insert_one — Mathlib

English

Including the identity element 1 in the generating set does not change the generated submonoid: closure(insert(1) s) = closure(s).

Русский

Добавление единицы 1 к порождающему множеству не меняет порожденный подмоном: closure(insert(1) s) = closure(s).

LaTeX

$$$\\operatorname{closure}(\\mathrm{insert}(1, s)) = \\operatorname{closure}(s)$$$

Lean4

@[to_additive (attr := simp)]
theorem closure_insert_one (s : Set M) : closure (insert 1 s) = closure s :=
  by
  rw [insert_eq, closure_union, sup_eq_right, closure_singleton_le_iff_mem]
  apply one_mem

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