measurableSet_B

Mathlib.Analysis.Calculus.FDeriv.Measurable

URI: https://scilib.ai/kg/mathlib#RightDerivMeasurableAux.measurableSet_B

English

The set B(f,K,r,s,ε) is a measurable set.

Русский

Множество B(f,K,r,s,ε) измеримо.

LaTeX

$$$\\text{MeasurableSet}\\ (B\_f\\ K\\ r\\ s\\ ε)$$$

Lean4

theorem measurableSet_B {K : Set F} {r s ε : ℝ} : MeasurableSet (B f K r s ε) :=
  .of_mem_nhdsGT fun _ hx => B_mem_nhdsGT hx

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru