opensMeasurableSpace_iff_forall_measurableSet

English

The structure OpensMeasurableSpace α is equivalent to the statement that every open set is measurable.

Русский

Структура OpensMeasurableSpace α эквивалентна утверждению, что каждый открытый множество измеримо.

LaTeX

$$$$ OpensMeasurableSpace α \iff (\forall s \subseteq α, IsOpen(s) \rightarrow MeasurableSet(s)). $$$$

Lean4

theorem opensMeasurableSpace_iff_forall_measurableSet [TopologicalSpace α] [MeasurableSpace α] :
    OpensMeasurableSpace α ↔ (∀ (s : Set α), IsOpen s → MeasurableSet s) :=
  by
  refine ⟨fun h s hs ↦ ?_, fun h ↦ ⟨generateFrom_le h⟩⟩
  exact OpensMeasurableSpace.borel_le _ <| GenerateMeasurable.basic _ hs

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