snd — Mathlib

English

If f: α → β×γ is quasi-measure-preserving from μ to ν×τ, then the second coordinate map x ↦ f(x).2 is quasi-measure-preserving from μ to τ.

Русский

Если f: α→β×γ сохраняет меру, то проекция на вторую координату сохраняет меру.

LaTeX

$$QuasiMeasurePreserving f (μ × ν) τ → QuasiMeasurePreserving (fun x => (f x).2) μ τ$$

Lean4

@[fun_prop]
protected theorem snd {f : α → β × γ} (hf : QuasiMeasurePreserving f μ (ν.prod τ)) :
    QuasiMeasurePreserving (fun x ↦ (f x).2) μ τ :=
  (quasiMeasurePreserving_snd (μ := ν) (ν := τ)).comp hf

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