exists_nonempty_inter_of_measure_univ_lt_tsum_measure

English

If the total measure of a universe exceeds the sum of measures of an indexed family of sets, then there exist indices i ≠ j with s_i ∩ s_j nonempty.

Русский

Если мера всего пространства больше суммы мер семейства множеств, то существуют i ≠ j такие, что s_i ∩ s_j не пусто.

LaTeX

$$$ μ(univ) < \sum' i, μ(s_i) \Rightarrow \exists i \neq j, (s_i \cap s_j).Nonempty $$$

Lean4

/-- Pigeonhole principle for measure spaces: if `∑' i, μ (s i) > μ univ`, then
one of the intersections `s i ∩ s j` is not empty. -/
theorem exists_nonempty_inter_of_measure_univ_lt_tsum_measure {m : MeasurableSpace α} (μ : Measure α) {s : ι → Set α}
    (hs : ∀ i, NullMeasurableSet (s i) μ) (H : μ (univ : Set α) < ∑' i, μ (s i)) :
    ∃ i j, i ≠ j ∧ (s i ∩ s j).Nonempty := by
  contrapose! H
  apply tsum_measure_le_measure_univ hs
  intro i j hij
  exact (disjoint_iff_inter_eq_empty.mpr (H i j hij)).aedisjoint

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