projectiveFamilyFun_empty — Mathlib

English

For every projective family P, the projective family value on the empty set is zero: projectiveFamilyFun P ∅ = 0.

Русский

Для любого проектирующего семейства P значение на пустом множестве равно нулю: projectiveFamilyFun P ∅ = 0.

LaTeX

$$$\operatorname{projectiveFamilyFun} P \emptyset = 0$$$

Lean4

theorem projectiveFamilyFun_empty (hP : IsProjectiveMeasureFamily P) : projectiveFamilyFun P ∅ = 0 := by
  rw [projectiveFamilyFun_congr hP (empty_mem_measurableCylinders α) (cylinder_empty ∅).symm MeasurableSet.empty,
    measure_empty]

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