instIsOpenUnitsOfContinuousInv — Mathlib

English

If a group M is equipped with a topology such that inversion is continuous, then the group of units U(M) is open in M.

Русский

Если у группы M задана топология, в которой инверсия непрерывна, то множество единиц U(M) открыто в M.

LaTeX

$$$\\mathrm{IsOpenUnits}\\, M$ при непрерывной инверсии$$

Lean4

instance (priority := 900) {M : Type*} [Group M] [TopologicalSpace M] [ContinuousInv M] : IsOpenUnits M where
  isOpenEmbedding_unitsVal := toUnits_homeomorph.symm.isOpenEmbedding

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