ball_subset_univBall_target — Mathlib

English

For any center c and radius r, the ball ball(c,r) is contained in the target of univBall(c,r).

Русский

Для любого центра c и радиуса r шар ball(c,r) содержится в целевой области univBall(c,r).

LaTeX

$$$\mathrm{ball}(c,r) \subseteq (\mathrm{univBall}(c,r)).\mathrm{target}.$$$

Lean4

theorem ball_subset_univBall_target (c : P) (r : ℝ) : ball c r ⊆ (univBall c r).target :=
  by
  by_cases hr : 0 < r
  · rw [univBall_target c hr]
  · rw [univBall, dif_neg hr]
    exact subset_univ _

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