mem_nhds_one — Mathlib

English

If S is a submonoid of a topological monoid M and its carrier is open, then S contains a neighborhood of the identity 1 in M.

Русский

Если S — подмоноид M и множество S открыто, то S содержит окрестность единицы 1 в M.

LaTeX

$$$S \\subseteq M\\;\\text{ Submonoid},\\; oS : IsOpen (S : Set M) \\Rightarrow S \\in \\mathcal{N}(1) $$$

Lean4

@[to_additive]
theorem mem_nhds_one (S : Submonoid M) (oS : IsOpen (S : Set M)) : (S : Set M) ∈ 𝓝 (1 : M) :=
  IsOpen.mem_nhds oS S.one_mem

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