normed_le_div_measure_closedBall_rIn

English

The real measure of a closed ball is finite: μ.real(closedBall(c,r)) < ∞.

Русский

Мера real замкнутого шара ограничена сверху: μ.real(closedBall(c,r)) < ∞.

LaTeX

$$$ \mu.real(\mathrm{closedBall}(c,r)) < \infty $$$

Lean4

theorem normed_le_div_measure_closedBall_rIn [μ.IsOpenPosMeasure] (x : E) :
    f.normed μ x ≤ 1 / μ.real (closedBall c f.rIn) :=
  by
  rw [normed_def]
  gcongr
  · exact ENNReal.toReal_pos (measure_closedBall_pos _ _ f.rIn_pos).ne' measure_closedBall_lt_top.ne
  · exact f.le_one
  · exact f.measure_closedBall_le_integral μ

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