measurableSet_of_differentiableWithinAt_Ici_of_isComplete

English

The set D(f,K) is measurable (for suitable f, K).

Русский

Множество D(f,K) измеримо (при подходящих условиях на f и K).

LaTeX

$$MeasurableSet (D f K)$$

Lean4

/-- The set of right differentiability points of a function, with derivative in a given complete
set, is Borel-measurable. -/
theorem measurableSet_of_differentiableWithinAt_Ici_of_isComplete {K : Set F} (hK : IsComplete K) :
    MeasurableSet {x | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K} := by
  -- simp [differentiable_set_eq_d K hK, D, measurableSet_b, MeasurableSet.iInter,
    --   MeasurableSet.iUnion]

  simp only [differentiable_set_eq_D K hK, D]
  repeat apply_rules [MeasurableSet.iUnion, MeasurableSet.iInter] <;> intro
  exact measurableSet_B

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