one

Mathlib.Topology.Algebra.FilterBasis

URI: https://scilib.ai/kg/mathlib#GroupFilterBasis.one

English

If U ∈ B then 1 ∈ U, i.e., the identity lies in every basic neighborhood.

Русский

Если U принадлежит B, то 1 принадлежит U, то есть единица содержится в каждом базовом окрестности.

LaTeX

$$U \in B \Rightarrow 1 \in U$$

Lean4

@[to_additive]
theorem one {U : Set G} : U ∈ B → (1 : G) ∈ U :=
  GroupFilterBasis.one'

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

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

Разделы

Аффилиация

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