mul_closure_one_eq

Mathlib.Topology.Algebra.Group.Pointwise

URI: https://scilib.ai/kg/mathlib#IsOpen.mul_closure_one_eq

← MathLib Explorer

English

If U is open, then U · closure({1}) = U.

Русский

Если U открытое, то U · closure({1}) = U.

LaTeX

$$$\\forall U \\subseteq G,\\ (\\text{IsOpen}(U)) \\Rightarrow U \\cdot \\overline{\\{1\\}} = U$$$

Lean4

@[to_additive]
theorem mul_closure_one_eq {U : Set G} (hU : IsOpen U) : U * (closure { 1 } : Set G) = U :=
  compl_mul_closure_one_eq_iff.1 (hU.isClosed_compl.mul_closure_one_eq)

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

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

Разделы

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

Аффилиация

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