eq_zero_of_isEmpty — Mathlib

English

Same principle as above for the projective family: emptiness forces the measure to be zero.

Русский

Та же идея: пустота пространства заставляет меру быть ноль.

LaTeX

$$$P I = 0\,\text{ for all } I\text{ when } (\prod_i \alpha_i) = \emptyset.$$$

Lean4

theorem eq_zero_of_isEmpty [h : IsEmpty (Π i, α i)] (hP : IsProjectiveMeasureFamily P) (I : Finset ι) : P I = 0 := by
  classical
  obtain ⟨i, hi⟩ := isEmpty_pi.mp h
  rw [hP (insert i I) I (I.subset_insert i)]
  have : IsEmpty (Π j : ↑(insert i I), α j) := by simp [hi]
  rw [(P (insert i I)).eq_zero_of_isEmpty]
  simp

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