instIsOpenUnitsOfDiscreteTopology

English

If a monoid M is equipped with a discrete topology, then the group of units U(M) is an open subset of M.

Русский

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

LaTeX

$$$\\mathrm{Units}(M) \\subseteq M$ открытое множество$$

Lean4

instance (priority := 900) (M : Type*) [Monoid M] [TopologicalSpace M] [DiscreteTopology M] : IsOpenUnits M where
  isOpenEmbedding_unitsVal :=
    .of_continuous_injective_isOpenMap Units.continuous_val Units.val_injective fun _ _ ↦ isOpen_discrete _

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