borelSpace — Mathlib

English

For a topological group G and a normal subgroup N that is closed, the quotient G ⧸ N is a Borel space.

Русский

Для топологической группы G и нормального замкнутого подгруппы N, факторпространство G ⧸ N является борелево-размеченным пространством.

LaTeX

$$BorelSpace (G ⧸ N)$$

Lean4

@[to_additive]
instance borelSpace {G : Type*} [TopologicalSpace G] [PolishSpace G] [Group G] [IsTopologicalGroup G]
    [MeasurableSpace G] [BorelSpace G] {N : Subgroup G} [N.Normal] [IsClosed (N : Set G)] : BorelSpace (G ⧸ N) :=
  ⟨continuous_mk.map_eq_borel mk_surjective⟩

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