mk — Mathlib · SciLib

English

If for every measurable s with w(s)=0 we have v(s)=0, then v ≪ᵥ w.

Русский

Если для каждого измеримого s с w(s)=0 выполняется v(s)=0, то v ≪ᵥ w.

LaTeX

$$((∀ ⦃s⦄, MeasurableSet s → w s = 0 → v s = 0) → v ≪ᵥ w)$$

Lean4

theorem mk (h : ∀ ⦃s : Set α⦄, MeasurableSet s → w s = 0 → v s = 0) : v ≪ᵥ w :=
  by
  intro s hs
  by_cases hmeas : MeasurableSet s
  · exact h hmeas hs
  · exact not_measurable v hmeas

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