nonempty_inter_of_measure_lt_add'

English

If a family s_i is directed by inclusion, then μ(⋃ i s_i) = ⨆ i μ(s_i).

Русский

Если семейство множеств упорядочено включением, то мера объединения равна верхней границе мер входящих множеств.

LaTeX

$$$ μ(⋃ i, s_i) = \sup_i μ(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 `s` is measurable. -/
theorem nonempty_inter_of_measure_lt_add' {m : MeasurableSpace α} (μ : Measure α) {s t u : Set α} (hs : MeasurableSet s)
    (h's : s ⊆ u) (h't : t ⊆ u) (h : μ u < μ s + μ t) : (s ∩ t).Nonempty :=
  by
  rw [add_comm] at h
  rw [inter_comm]
  exact nonempty_inter_of_measure_lt_add μ hs h't h's h

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