measure_le_lt_top — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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