fst — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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