singularPart_of_subset_compl_mutuallySingularSetSlice

English

If s is contained in the complement of the slice, then the singular part over s is zero.

Русский

Если s ⊆ complement(mutuallySingularSetSlice), то singularPart κ η a s = 0.

LaTeX

$$$ singularPart(\kappa, \eta)(a)(s) = 0 \quad\text{whenever } s \subseteq (mutuallySingularSetSlice(\kappa, \eta)(a))^{c}$$$

Lean4

theorem singularPart_of_subset_compl_mutuallySingularSetSlice [IsSFiniteKernel κ] [IsFiniteKernel η] {a : α} {s : Set γ}
    (hs : s ⊆ (mutuallySingularSetSlice κ η a)ᶜ) : singularPart κ η a s = 0 :=
  measure_mono_null hs (singularPart_compl_mutuallySingularSetSlice κ η a)

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