exists_pos_lt_subset_ball — Mathlib

English

The neighborhood filter at x has a basis consisting of closed balls with positive radii.

Русский

Окрежность в x имеет базис из замкнутых шаров с положительным радиусом.

LaTeX

$$∃ basis from {closedBall x r : r>0}$$

Lean4

nonrec theorem exists_pos_lt_subset_ball {R : ℝ} {s : Set E} {x : E} (hR : 0 < R) (hs : IsClosed s) (h : s ⊆ ball x R) :
    ∃ r ∈ Ioo 0 R, s ⊆ ball x r := by
  rw [ball_eq_preimage, ← image_subset_iff] at h
  rcases exists_pos_lt_subset_ball hR (toEuclidean.isClosed_image.2 hs) h with ⟨r, hr, hsr⟩
  exact ⟨r, hr, image_subset_iff.1 hsr⟩

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