ball_subset_closedBall — Mathlib

English

For any x and r, the ball is contained in the corresponding closedBall: ball p x r ⊆ closedBall p x r.

Русский

Для любых x и r шар содержится в соответствующем замкнутом шаре: ball p x r ⊆ closedBall p x r.

LaTeX

$$$\\mathrm{ball}_p(x,r) \\subseteq \\mathrm{closedBall}_p(x,r)$$$

Lean4

theorem ball_subset_closedBall (x r) : ball p x r ⊆ closedBall p x r := fun _ h =>
  (mem_closedBall _).mpr ((mem_ball _).mp h).le

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