absolutelyContinuous_boolKernel_comp_right

English

If π{true} ≠ 0, then ν ≪ Kernel.boolKernel μ ν ∘ₘ π.

Русский

Если π{true} ≠ 0, тогда ν ≪ Kernel.boolKernel μ ν ∘ₘ π.

LaTeX

$$$\\pi\\{true\\} \\neq 0 \\Rightarrow ν \\ll Kernel.boolKernel μ ν \\circ_{m} π$$$

Lean4

theorem absolutelyContinuous_boolKernel_comp_right (μ ν : Measure α) (hπ : π { true } ≠ 0) :
    ν ≪ Kernel.boolKernel μ ν ∘ₘ π :=
  boolKernel_comp_measure _ _ _ ▸ (Measure.absolutelyContinuous_smul hπ).add_right _

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