closedBall_subset_closedBall — Mathlib

English

If ε1 ≤ ε2, then the closed ball centered at x with radius ε1 is contained in the closed ball centered at x with radius ε2.

Русский

Если ε1 ≤ ε2, то замкнутый шар с центром в x и радиусом ε1 содержится в замкнутом шаре с центром в x и радиусом ε2.

LaTeX

$$$\\overline{\\mathrm{B}}(x,\\varepsilon_1) \\subseteq \\overline{\\mathrm{B}}(x,\\varepsilon_2) \\text{ for } \\varepsilon_1 \\le \\varepsilon_2$$$

Lean4

@[gcongr]
theorem closedBall_subset_closedBall (h : ε₁ ≤ ε₂) : closedBall x ε₁ ⊆ closedBall x ε₂ := fun _y (yx : _ ≤ ε₁) =>
  le_trans yx h

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