exists_measure_pos_of_not_measure_iUnion_null

English

Let ι be countable and s: ι → Set α. If μ(⋃_{n} s(n)) ≠ 0, then there exists n with μ(s(n)) > 0.

Русский

Пусть индекс ι счетный и s(n) наборы. Если μ(⋃_{n} s(n)) ≠ 0, то существует n такой, что μ(s(n)) > 0.

LaTeX

$$∃ n, 0 < μ(s(n))$$

Lean4

theorem exists_measure_pos_of_not_measure_iUnion_null [Countable ι] {s : ι → Set α} (hs : μ (⋃ n, s n) ≠ 0) :
    ∃ n, 0 < μ (s n) := by
  contrapose! hs
  exact measure_iUnion_null fun n => nonpos_iff_eq_zero.1 (hs n)

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