dependsOn_of_piLE — Mathlib

English

If a function is measurable with respect to the σ-algebra generated by finitely many coordinates, then it depends only on those coordinates.

Русский

Если функция измерима относительно σ-алгебры, порожденной конечным числом координат, она зависит только от этих координат.

LaTeX

$$$$ \text{DependsOn } f (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_piLE [TopologicalSpace Z] [PseudoMetrizableSpace Z] [T1Space Z]
    (hf : StronglyMeasurable[piLE i] f) : DependsOn f (Iic i) :=
  dependsOn_iff_factorsThrough.2 hf.factorsThrough

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