measure_ball_pos — Mathlib

English

For EMetric spaces, μ(ball x r) > 0 whenever r ≠ 0 and μ is open-positive.

Русский

В пространствах EMetric, если r ≠ 0, то мера шара положительна при открыто-положительной мере μ.

LaTeX

$$$\\forall x,\\forall r \\; (r \\neq 0) \\Rightarrow 0 < \\mu(\\mathrm{ball}\,x\,r).$$$

Lean4

theorem measure_ball_pos (x : X) {r : ℝ≥0∞} (hr : r ≠ 0) : 0 < μ (ball x r) :=
  isOpen_ball.measure_pos μ ⟨x, mem_ball_self hr.bot_lt⟩

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