closedBall_subset_closedBall — Mathlib

English

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

Русский

Если ε1 ≤ ε2, то B̄(x, ε1) ⊆ B̄(x, ε2).

LaTeX

$$$ \overline{B}(x, \varepsilon_1) \subseteq \overline{B}(x, \varepsilon_2) \quad\text{whenever } \varepsilon_1 \le \varepsilon_2 $$$

Lean4

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

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