dependsOn_of_piFinset — Mathlib

English

If f depends only on coordinates in a finite set s, then there exists h: s → Z with f = h ∘ f|_s.

Русский

Если f зависит только от координат в конечном множестве s, существует h: s → Z с f = h ∘ f|_s.

LaTeX

$$$$ \exists h : s \to Z, \; f = h \circ (\text{projection to } s). $$$$

Lean4

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

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