English
If the union of t_i over i ∈ s has real measure strictly larger than the sum of real measures of t_i, then some pair t_i ∩ t_j is nonempty.
Русский
Если μ.real(univ) < ∑ μ.real(t_i) для i в s, то найдутся i ≠ j с t_i ∩ t_j ≠ ∅.
LaTeX
$$… (формула в тексте)$$
Lean4
/-- Pigeonhole principle for measure spaces: if `s` is a `Finset` and
`∑ i ∈ s, μ.real (t i) > μ.real univ`, then one of the intersections `t i ∩ t j` is not empty. -/
theorem exists_nonempty_inter_of_measureReal_univ_lt_sum_measureReal [IsFiniteMeasure μ] {s : Finset ι} {t : ι → Set α}
(h : ∀ i ∈ s, MeasurableSet (t i)) (H : μ.real univ < ∑ i ∈ s, μ.real (t i)) :
∃ i ∈ s, ∃ j ∈ s, ∃ _h : i ≠ j, (t i ∩ t j).Nonempty :=
by
apply exists_nonempty_inter_of_measure_univ_lt_sum_measure μ (fun i mi ↦ (h i mi).nullMeasurableSet)
simp only [Measure.real] at H
apply (ENNReal.toReal_lt_toReal (measure_ne_top _ _) _).1
· convert H
rw [ENNReal.toReal_sum (fun i hi ↦ measure_ne_top _ _)]
· exact (ENNReal.sum_lt_top.mpr (fun i hi ↦ measure_lt_top ..)).ne
