borelSpace — Mathlib

English

For any setoid s on a Polish space X, the quotient space X/ s carries a Borel space structure: BorelSpace (Quotient s).

Русский

Для произвольной эквивалентности на полическом пространстве X, фактор-пространство X/ s обладает борелевой структурой: BorelSpace (Quotient s).

LaTeX

$$BorelSpace (Quotient s)$$

Lean4

instance borelSpace {X : Type*} [TopologicalSpace X] [PolishSpace X] [MeasurableSpace X] [BorelSpace X] {s : Setoid X}
    [T0Space (Quotient s)] [SecondCountableTopology (Quotient s)] : BorelSpace (Quotient s) :=
  ⟨continuous_quotient_mk'.map_eq_borel Quotient.mk'_surjective⟩

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