condKernel_def — Mathlib

English

For ρ on α × ℝ with κ and hκ: ρ = ρ.fst.compProd κ, κ equalscondKernel on a.e. under ρ.fst when κ is s-finite.

Русский

Для ρ на α × ℝ с κ и hκ: ρ = ρ.fst.compProd κ; при условии с-финитности κ верна полуравенство κ = condKernel почти по ρ.fst.

LaTeX

$$$eq\\_condKernel\\_of\\_measure\\_eq\\_compProd\\_real$$$

Lean4

theorem condKernel_def : eta_helper Eq✝ @condKernel.{} @(delta% @definition✝) :=
  by
  intros
  delta condKernel
  rw [show wrapped✝ = ⟨@definition✝.{}, rfl✝⟩ from Subtype.ext✝ wrapped✝.2.symm✝]
  rfl

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