isOpen_of_one_mem_interior — Mathlib

English

If a subgroup H of a topological group G contains the identity in its interior, then H is open.

Русский

Если единица включена во внутренность подгруппы H в топологической группе G, то H открыта.

LaTeX

$$$$ \\text{If } 1 \\in \\operatorname{int}(H), \\text{ then } H \\text{ is open}. $$$$

Lean4

/-- If a subgroup of a topological group has `1` in its interior, then it is open. -/
@[to_additive /-- If a subgroup of an additive topological group has `0` in its interior, then it is
    open. -/
    ]
theorem isOpen_of_one_mem_interior [ContinuousMul G] (H : Subgroup G) (h_1_int : (1 : G) ∈ interior (H : Set G)) :
    IsOpen (H : Set G) :=
  isOpen_of_mem_nhds H <| mem_interior_iff_mem_nhds.1 h_1_int

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