absolutelyContinuous_compProd_left_iff

English

Under suitable finiteness and nonzero assumptions, μ ⊗ κ ≪ ν ⊗ κ iff μ ≪ ν.

Русский

При подходящих условиях конечности и не нуля, μ ⊗ κ ⪯ ν ⊗ κ тогда и только тогда μ ⪯ ν.

LaTeX

$$$[SFinite(\\mu)] [SFinite(\\nu)] [IsSFiniteKernel(\\kappa)] [\\forall a, NeZero(\\kappa(a))] : (μ ⊗ₘ κ) \\ll (ν ⊗ₘ κ) \\iff μ \\ll ν$$$

Lean4

theorem absolutelyContinuous_compProd_left_iff [SFinite μ] [SFinite ν] [IsSFiniteKernel κ] [∀ a, NeZero (κ a)] :
    μ ⊗ₘ κ ≪ ν ⊗ₘ κ ↔ μ ≪ ν :=
  ⟨absolutelyContinuous_of_compProd, fun h ↦ h.compProd_left κ⟩

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