exists_subset_lt_add — Mathlib

English

If H is inner regular and μ(U) finite, then for any ε > 0 there exists K ⊆ U with p(K) and μ(U) < μ(K) + ε.

Русский

Если H внутренняя регулярность, и μ(U) конечна, то существует K ⊆ U с p(K) и μ(U) < μ(K) + ε.

LaTeX

$$∃ K ⊆ U, p K ∧ μ U < μ K + ε$$

Lean4

theorem exists_subset_lt_add (H : InnerRegularWRT μ p q) (h0 : p ∅) (hU : q U) (hμU : μ U ≠ ∞) (hε : ε ≠ 0) :
    ∃ K, K ⊆ U ∧ p K ∧ μ U < μ K + ε := by
  rcases eq_or_ne (μ U) 0 with h₀ | h₀
  · refine ⟨∅, empty_subset _, h0, ?_⟩
    rwa [measure_empty, h₀, zero_add, pos_iff_ne_zero]
  · rcases H hU _ (ENNReal.sub_lt_self hμU h₀ hε) with ⟨K, hKU, hKc, hrK⟩
    exact ⟨K, hKU, hKc, ENNReal.lt_add_of_sub_lt_right (Or.inl hμU) hrK⟩

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