nonempty_inter_of_measure_lt_add — Mathlib

English

If t is countable, then the measure of the union of s_i over i ∈ t equals the supremum over i ∈ t of μ(s_i).

Русский

Если t счётно, мера объединения s_i по i ∈ t равна верхней границе по i ∈ t величин μ(s_i).

LaTeX

$$$ μ(⋃ i ∈ t, s_i) = \sup_{i ∈ t} μ(s_i) $$$

Lean4

/-- If two sets `s` and `t` are included in a set `u`, and `μ s + μ t > μ u`,
then `s` intersects `t`. Version assuming that `t` is measurable. -/
theorem nonempty_inter_of_measure_lt_add {m : MeasurableSpace α} (μ : Measure α) {s t u : Set α} (ht : MeasurableSet t)
    (h's : s ⊆ u) (h't : t ⊆ u) (h : μ u < μ s + μ t) : (s ∩ t).Nonempty :=
  by
  rw [← Set.not_disjoint_iff_nonempty_inter]
  contrapose! h
  calc
    μ s + μ t = μ (s ∪ t) := (measure_union h ht).symm
    _ ≤ μ u := measure_mono (union_subset h's h't)

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