measure_gt_lt_top — Mathlib

English

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

Русский

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

LaTeX

$$$\\forall \\varepsilon>0,\\ \\mu\\{a:\\varepsilon

Lean4

/-- If `f` is `ℝ`-valued and integrable, then for any `c > 0` the set `{x | f x > c}` has finite
measure. -/
theorem measure_gt_lt_top {f : α → ℝ} (hf : Integrable f μ) {ε : ℝ} (ε_pos : 0 < ε) : μ {a : α | ε < f a} < ∞ :=
  lt_of_le_of_lt (measure_mono (fun _ hx ↦ (Set.mem_setOf_eq ▸ hx).le)) (Integrable.measure_ge_lt_top hf ε_pos)

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