measure_ball_lt_top

Mathlib.MeasureTheory.Measure.Typeclasses.Finite

URI: https://scilib.ai/kg/mathlib#MeasureTheory.measure_ball_lt_top

← MathLib Explorer

English

Similarly, the measure of the open ball around x with radius r is finite.

Русский

Аналогично, мера открытого шара вокруг x с радиусом r конечна.

LaTeX

$$$\mu( B(x,r) ) < \infty$$$

Lean4

theorem measure_ball_lt_top [PseudoMetricSpace α] [ProperSpace α] {μ : Measure α} [IsFiniteMeasureOnCompacts μ] {x : α}
    {r : ℝ} : μ (Metric.ball x r) < ∞ :=
  Metric.isBounded_ball.measure_lt_top

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru