closure_sdiff_singleton_one

Mathlib.Algebra.Group.Submonoid.Basic

URI: https://scilib.ai/kg/mathlib#Submonoid.closure_sdiff_singleton_one

← MathLib Explorer

English

The closure of s minus the identity equals the closure of s: closure(s \\ {1}) = closure(s).

Русский

Замыкание множества s без 1 равно замыканию s: closure(s \\ {1}) = closure(s).

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem closure_sdiff_singleton_one (s : Set M) : closure (s \ { 1 }) = closure s :=
  closure_sdiff_eq_closure <| by simp [one_mem]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru