measurableSet — Mathlib

English

If s is an OrdConnected subset of a linearly ordered space α with a suitable topology, then s is a measurable set.

Русский

Если s — OrdConnectedsubset пространства α с линейным порядком и допустимой топологией, то s — измеримо.

LaTeX

$$$\text{OrdConnected}(s)\Rightarrow \ MeasurableSet(s)$$$

Lean4

theorem measurableSet (h : OrdConnected s) : MeasurableSet s :=
  by
  let u := ⋃ (x ∈ s) (y ∈ s), Ioo x y
  have huopen : IsOpen u := isOpen_biUnion fun _ _ => isOpen_biUnion fun _ _ => isOpen_Ioo
  have humeas : MeasurableSet u := huopen.measurableSet
  have hfinite : (s \ u).Finite := s.finite_diff_iUnion_Ioo
  have : u ⊆ s := iUnion₂_subset fun x hx => iUnion₂_subset fun y hy => Ioo_subset_Icc_self.trans (h.out hx hy)
  rw [← union_diff_cancel this]
  exact humeas.union hfinite.measurableSet

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