absolutelyContinuous_compProd_right_iff

English

For [SFinite μ], μ ⊗ κ ≪ μ ⊗ η if and only if ∀ᵐ a ∂ μ, κ a ≪ η a.

Русский

Для [SFinite μ] выполняется μ ⊗ κ ≪ μ ⊗ η тогда и только тогда, когда ∀ᵐ a ∂ μ, κ(a) ≪ η(a).

LaTeX

$$$[SFinite \\mu] \\Rightarrow (\\mu ⊗ κ) \\ll (\\mu ⊗ η) \\iff (\\forall^{\\text{ae}} a\\partial μ,\\ κ(a) \\ll η(a)).$$$

Lean4

theorem absolutelyContinuous_compProd_right_iff [SFinite μ] : μ ⊗ₘ κ ≪ μ ⊗ₘ η ↔ ∀ᵐ a ∂μ, κ a ≪ η a :=
  ⟨AbsolutelyContinuous.kernel_of_compProd, AbsolutelyContinuous.compProd_right⟩

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