dependsOn_of_piFinset — Mathlib

English

If g is strongly measurable on a product space indexed by I and depends only on a finite set s, then g factors through the projection to s.

Русский

Если g сильно измерима на произведении по индексу I и зависит только от конечного множества координат s, тогда g факторизуется через проекцию на s.

LaTeX

$$$$ \text{g is determined by coordinates in } s. $$$$

Lean4

/-- If a function is strongly measurable with respect to the σ-algebra generated by the
first coordinates, then it only depends on those first coordinates. -/
theorem dependsOn_of_piFinset [TopologicalSpace Z] [PseudoMetrizableSpace Z] [T1Space Z]
    (hf : StronglyMeasurable[piFinset s] f) : DependsOn f s :=
  dependsOn_iff_factorsThrough.2 hf.factorsThrough

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