exists_nonempty_inter_of_measure_univ_lt_sum_measure

English

For a finite index set s and sets t_i with μ(univ) < sum μ(t_i), there exist i,j ∈ s with i ≠ j and (t_i ∩ t_j) nonempty.

Русский

Для конечного индекса s и множеств t_i при μ(univ) < ∑ μ(t_i) найдутся i ≠ j с i,j ∈ s и (t_i ∩ t_j) непусто.

LaTeX

$$$ μ(univ) < \sum_{i \in s} μ(t_i) \Rightarrow \exists i \in s, \exists j \in s, i ≠ j, (t_i ∩ t_j).Nonempty $$$

Lean4

/-- Pigeonhole principle for measure spaces: if `s` is a `Finset` and
`∑ i ∈ s, μ (t i) > μ univ`, then one of the intersections `t i ∩ t j` is not empty. -/
theorem exists_nonempty_inter_of_measure_univ_lt_sum_measure {m : MeasurableSpace α} (μ : Measure α) {s : Finset ι}
    {t : ι → Set α} (h : ∀ i ∈ s, NullMeasurableSet (t i) μ) (H : μ (univ : Set α) < ∑ i ∈ s, μ (t i)) :
    ∃ i ∈ s, ∃ j ∈ s, ∃ _h : i ≠ j, (t i ∩ t j).Nonempty :=
  by
  contrapose! H
  apply sum_measure_le_measure_univ h
  intro i hi j hj hij
  exact (disjoint_iff_inter_eq_empty.mpr (H i hi j hj hij)).aedisjoint

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