pi_hyperplane — Mathlib

English

If i has no atoms under μ_i, then the hyperplane {f : f_i = x} has measure zero under π μ.

Русский

Если в i-й компоненте μ_i нет атомов, гиперплоскость {f: f_i = x} имеет нулевую меру по π μ.

LaTeX

$$$\pi\mu(\{f : f_i = x\}) = 0$$$

Lean4

theorem pi_hyperplane (i : ι) [NoAtoms (μ i)] (x : α i) : Measure.pi μ {f : ∀ i, α i | f i = x} = 0 :=
  show Measure.pi μ (eval i ⁻¹' { x }) = 0 from pi_eval_preimage_null _ (measure_singleton x)

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