ball_subset_ball — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[gcongr]
theorem ball_subset_ball (h : ε₁ ≤ ε₂) : ball x ε₁ ⊆ ball x ε₂ := fun _y (yx : _ < ε₁) => lt_of_lt_of_le yx h

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