isOpen_mono — Mathlib

English

OpenSubgroup G carries a natural order by inclusion; the ambient order is visible via the partial order instance.

Русский

OpenSubgroup G имеет естественный порядок по включению; природный порядок задаётся через инстанс частичного порядка.

LaTeX

$$$$ \\text{OpenSubgroup}(G) \\text{ is a poset under } \\subseteq. $$$$

Lean4

@[to_additive]
theorem isOpen_mono [ContinuousMul G] {H₁ H₂ : Subgroup G} (h : H₁ ≤ H₂) (h₁ : IsOpen (H₁ : Set G)) :
    IsOpen (H₂ : Set G) :=
  isOpen_of_mem_nhds _ <| Filter.mem_of_superset (h₁.mem_nhds <| one_mem H₁) h

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