standardBorelSpace_of_discreteMeasurableSpace

English

The AnalyticSet is defined as the class of sets that are projections of Borel sets from Polish spaces.

Русский

AnalyticSet определяется как класс множеств, являющихся проекциями бореллевых множеств полских пространств.

LaTeX

$$$ AnalyticSet := \{ S \subseteq α : \exists P\, (\text{Polish}), B \subseteq P \text{ Borel}, f: P \to α, S = f[B] \}$$$

Lean4

instance (priority := 100) standardBorelSpace_of_discreteMeasurableSpace [DiscreteMeasurableSpace α] [Countable α] :
    StandardBorelSpace α :=
  let _ : TopologicalSpace α := ⊥
  have : DiscreteTopology α := ⟨rfl⟩
  inferInstance

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