exists_pos_measure_of_cover — Mathlib

English

If a countable cover of the space by sets U_i equals the whole space and μ ≠ 0, then some U_i has positive μ-measure.

Русский

Если счётное покрытие пространства множествами U_i охватывает всю пространство и μ ≠ 0, тогда некоторые U_i имеют положительную меру.

LaTeX

$$$\exists i, μ(U_i) > 0$ given $⋃_i U_i = \mathrm{univ}$ and $μ \ne 0$$$

Lean4

theorem exists_pos_measure_of_cover [Countable ι] {U : ι → Set α} (hU : ⋃ i, U i = univ) (hμ : μ ≠ 0) :
    ∃ i, 0 < μ (U i) := by
  contrapose! hμ with H
  rw [← measure_univ_eq_zero, ← hU]
  exact measure_iUnion_null fun i => nonpos_iff_eq_zero.1 (H i)

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