inducedOuterMeasure_exists_set — Mathlib

English

For Nat-indexed family of sets, the inequality extend_iUnion_nat holds: extend m (⋃ i, s i) ≤ ∑' i, extend m (s i).

Русский

Для семейства по Nat выполняется неравенство extend_iUnion_nat: extend m (⋃ i, s i) ≤ ∑' i, extend m (s i).

LaTeX

$$$\\mathrm{extend}\\ m(\\bigcup_{i} s_i) \\le \\sum_{i}^{\\prime} \\mathrm{extend}\\ m(s_i)$$$

Lean4

theorem inducedOuterMeasure_exists_set {s : Set α} (hs : inducedOuterMeasure m P0 m0 s ≠ ∞) {ε : ℝ≥0∞} (hε : ε ≠ 0) :
    ∃ t : Set α, P t ∧ s ⊆ t ∧ inducedOuterMeasure m P0 m0 t ≤ inducedOuterMeasure m P0 m0 s + ε :=
  by
  have h := ENNReal.lt_add_right hs hε
  conv at h =>
    lhs
    rw [inducedOuterMeasure_eq_iInf _ msU m_mono]
  simp only [iInf_lt_iff] at h
  rcases h with ⟨t, h1t, h2t, h3t⟩
  exact ⟨t, h1t, h2t, le_trans (le_of_eq <| inducedOuterMeasure_eq' _ msU m_mono h1t) (le_of_lt h3t)⟩

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