measure_ge_lt_top — Mathlib

English

If f is integrable and ε>0, then the set {a : ε ≤ f(a)} has finite measure.

Русский

Пусть f интегрируема и ε>0. Тогда множество {a: ε ≤ f(a)} имеет конечную меру.

LaTeX

$$$\\forall \\varepsilon>0,\\ \\mu\\{a:\\varepsilon\\le f(a)\\}<\\infty$$$

Lean4

/-- If `f` is `ℝ`-valued and integrable, then for any `c > 0` the set `{x | f x ≥ c}` has finite
measure. -/
theorem measure_ge_lt_top {f : α → ℝ} (hf : Integrable f μ) {ε : ℝ} (ε_pos : 0 < ε) : μ {a : α | ε ≤ f a} < ∞ :=
  by
  refine lt_of_le_of_lt (measure_mono ?_) (hf.measure_norm_ge_lt_top ε_pos)
  intro x hx
  simp only [Real.norm_eq_abs, Set.mem_setOf_eq] at hx ⊢
  exact hx.trans (le_abs_self _)

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