isClopen — Mathlib

English

Under continuous multiplication, an open subgroup is clopen (both open and closed).

Русский

При непрерывном умножении открытая подгруппа является и открытой, и замкнутой.

LaTeX

$$$\forall G\, [\mathrm{ContinuousMul}(G)],\ \forall U \in \mathrm{OpenSubgroup}(G):\ \mathrm{IsClopen}(U)$$$

Lean4

@[to_additive]
theorem isClopen [ContinuousMul G] (U : OpenSubgroup G) : IsClopen (U : Set G) :=
  ⟨U.isClosed, U.isOpen⟩

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