English
If G is a topological Polish group and N a subgroup, then the coset space G ⧸ N is a Borel space.
Русский
Пусть G — топологическая полская группа, N — подгруппа; косетное пространство G/N является борелевым пространством.
LaTeX
$$BorelSpace (G ⧸ N)$$
Lean4
/-- When the subgroup `N < G` is not necessarily `Normal`, we have a `CosetSpace` as opposed
to `QuotientGroup` (the next `instance`).
TODO: typeclass inference should normally find this, but currently doesn't.
E.g., `MeasurableSMul G (G ⧸ Γ)` fails to synthesize, even though `G ⧸ Γ` is the quotient
of `G` by the action of `Γ`; it seems unable to pick up the `BorelSpace` instance. -/
@[to_additive AddCosetSpace.borelSpace]
instance borelSpace {G : Type*} [TopologicalSpace G] [PolishSpace G] [Group G] [MeasurableSpace G] [BorelSpace G]
{N : Subgroup G} [T2Space (G ⧸ N)] [SecondCountableTopology (G ⧸ N)] : BorelSpace (G ⧸ N) :=
Quotient.borelSpace
