mk — Mathlib · SciLib

English

Given a measurable s, if v is null on all parts of s and w is null on all parts of s^c, then v ⟂ᵥ w.

Русский

Если для измеримого s векторная мера v равна нулю на всех подмножественных частях s, а w нулю на всех частях s^c, то v ⟂ᵥ w.

LaTeX

$$MutuallySingular.mk s hs h₁ h₂$$

Lean4

theorem mk (s : Set α) (hs : MeasurableSet s) (h₁ : ∀ t ⊆ s, MeasurableSet t → v t = 0)
    (h₂ : ∀ t ⊆ sᶜ, MeasurableSet t → w t = 0) : v ⟂ᵥ w :=
  by
  refine ⟨s, hs, fun t hst => ?_, fun t hst => ?_⟩ <;> by_cases ht : MeasurableSet t
  · exact h₁ t hst ht
  · exact not_measurable v ht
  · exact h₂ t hst ht
  · exact not_measurable w ht

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