instIsClosedCoePathComponentOne — Mathlib

English

The path component of the identity in a locally path-connected group is a closed subset (indeed clopen) and forms an open normal subgroup.

Русский

Компонента пути тождеству в локально путево связной группе замкнута и образует открытую нормальную подгруппу (на самом деле — открыта и замкнута).

LaTeX

$$$IsOpen (pathComponent 1)$$$

Lean4

@[to_additive]
instance [Group G] [IsTopologicalGroup G] [LocPathConnectedSpace G] :
    IsClosed (OpenNormalSubgroup.pathComponentOne G : Set G) :=
  .pathComponent 1

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