exists_pos_ball

Mathlib.MeasureTheory.Measure.Typeclasses.Finite

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

English

There exists n with μ(ball(x,n)) > 0.

Русский

Существует n, такое что μ(шар(x,n)) > 0.

LaTeX

$$$\exists n, μ(\mathrm{Ball}(x,n)) > 0$$$

Lean4

theorem exists_pos_ball [PseudoMetricSpace α] (x : α) (hμ : μ ≠ 0) : ∃ n : ℕ, 0 < μ (Metric.ball x n) :=
  exists_pos_preimage_ball id x hμ

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

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

Разделы

Аффилиация

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