quasiMeasurePreserving_eval — Mathlib

English

For each i, eval_i is quasi-measure-preserving from the product measure to μ_i.

Русский

Для каждого i функция eval_i является квази-меропереносной от произведённой меры π μ к μ_i.

LaTeX

$$QuasiMeasurePreserving(\mathrm{eval}_i,\, \pi\mu,\, \mu_i)$$

Lean4

theorem quasiMeasurePreserving_eval (i : ι) : QuasiMeasurePreserving (Function.eval i) (Measure.pi μ) (μ i) := by
  classical
  refine ⟨by fun_prop, AbsolutelyContinuous.mk fun s hs h2s => ?_⟩
  rw [map_apply (by fun_prop) hs, pi_eval_preimage_null μ h2s]

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