absolutelyContinuous_boolKernel_comp_left

English

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

Русский

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

LaTeX

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

Lean4

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

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