isBounded_closedBall — Mathlib

English

Closed balls are bounded: for any x and r, the set {y : dist(y,x) ≤ r} is bounded.

Русский

Замкнутые шары ограничены: для любого x и r множество {y : dist(y,x) ≤ r} ограничено.

LaTeX

$$IsBounded(ClosedBall(x,r))$$

Lean4

/-- Closed balls are bounded -/
theorem isBounded_closedBall : IsBounded (closedBall x r) :=
  isBounded_iff.2
    ⟨r + r, fun y hy z hz =>
      calc
        dist y z ≤ dist y x + dist z x := dist_triangle_right _ _ _
        _ ≤ r + r := add_le_add hy hz⟩

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