mem_closure_singleton_self

Mathlib.Algebra.Group.Subgroup.Lattice

URI: https://scilib.ai/kg/mathlib#Subgroup.mem_closure_singleton_self

← MathLib Explorer

English

For any x in a group, x ∈ closure({x}).

Русский

Для любой x в группе, x принадлежит closure({x}).

LaTeX

$$$ x \in \mathrm{closure}(\{x\}) $$$

Lean4

@[to_additive (attr := simp)]
theorem mem_closure_singleton_self (x : G) : x ∈ closure ({ x } : Set G) := by
  simpa [-subset_closure] using subset_closure (k := { x })

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

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

Разделы

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

Аффилиация

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