ball_subset — Mathlib

English

If edist(x,y) ≠ ∞ and edist(x,y) + ε1 ≤ ε2, then B(x,ε1) ⊆ B(y,ε2).

Русский

Если edist(x,y) ≠ ∞ и edist(x,y) + ε1 ≤ ε2, тогда B(x,ε1) ⊆ B(y,ε2).

LaTeX

$$$\\operatorname{edist}(x,y) \\neq \\infty \\wedge (\\operatorname{edist}(x,y) + \\varepsilon_1 \\le \\varepsilon_2) \\Rightarrow \\mathrm{ball}(x,\\varepsilon_1) \\subseteq \\mathrm{ball}(y,\\varepsilon_2)$$$

Lean4

theorem ball_subset (h : edist x y + ε₁ ≤ ε₂) (h' : edist x y ≠ ∞) : ball x ε₁ ⊆ ball y ε₂ := fun z zx =>
  calc
    edist z y ≤ edist z x + edist x y := edist_triangle _ _ _
    _ = edist x y + edist z x := (add_comm _ _)
    _ < edist x y + ε₁ := (ENNReal.add_lt_add_left h' zx)
    _ ≤ ε₂ := h

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