closedBall_mem_nhds_of_mem — Mathlib

English

If a point lies inside an open ball around some center, the corresponding closed ball around that center is a neighborhood of that point.

Русский

Если точка лежит внутри открытого шара вокруг некоторого центра, соответствующий замкнутый шар вокруг этого центра является окрестностью этой точки.

LaTeX

$$x ∈ ball(c, ε) → closedBall(c, ε) ∈ 𝓝(x)$$

Lean4

theorem closedBall_mem_nhds_of_mem {x c : α} {ε : ℝ} (h : x ∈ ball c ε) : closedBall c ε ∈ 𝓝 x :=
  mem_of_superset (isOpen_ball.mem_nhds h) ball_subset_closedBall

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