mem_nhds_one

Mathlib.Topology.Algebra.OpenSubgroup

URI: https://scilib.ai/kg/mathlib#OpenSubgroup.mem_nhds_one

English

For any open subgroup U, the set U is a neighborhood of 1 in G.

Русский

Для любой открытой подгруппы U множество U является окрестностью единицы в G.

LaTeX

$$$(U : \mathrm{Set}G) \in \mathcal{N}(1) $$$

Lean4

@[to_additive]
theorem mem_nhds_one : (U : Set G) ∈ 𝓝 (1 : G) :=
  U.isOpen.mem_nhds U.one_mem

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

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

Разделы

Аффилиация

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