meas_ge_lt_top' — Mathlib

English

If f ∈ MemLp with p ≠ 0, ∞, then μ{x | ε ≤ ‖f x‖₊} < ∞ for ε ≠ 0.

Русский

Если f ∈ MemLp, p ≠ 0, ∞, тогда μ{x: ε ≤ ‖f(x)‖₊} < ∞ для ε ≠ 0.

LaTeX

$$$$μ\\{x \\,|\\, ε ≤ \\|f(x)\\|_{+} \\} < ∞.$$$$

Lean4

theorem meas_ge_lt_top' {μ : Measure α} {f : α → E} (hℒp : MemLp f p μ) (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ∞)
    {ε : ℝ≥0∞} (hε : ε ≠ 0) : μ {x | ε ≤ ‖f x‖₊} < ∞ :=
  by
  by_cases h : ε = ∞
  · simp [h]
  exact hℒp.meas_ge_lt_top'_enorm hp_ne_zero hp_ne_top hε (by simp)

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