isBounded_ball

Mathlib.Topology.MetricSpace.Bounded

URI: https://scilib.ai/kg/mathlib#Metric.isBounded_ball

English

Open balls are bounded: for any x,r, the ball B(x,r) is bounded.

Русский

Открытые шары ограничены: для любого x и r множество B(x,r) ограничено.

LaTeX

$$IsBounded(Ball(x,r))$$

Lean4

/-- Open balls are bounded -/
theorem isBounded_ball : IsBounded (ball x r) :=
  isBounded_closedBall.subset ball_subset_closedBall

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

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

Разделы

Аффилиация

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