singleton_eq_inter_Icc — Mathlib

English

For every real b, the singleton {b} equals the intersection of the closed intervals Icc(b − r, b + r) for all positive r.

Русский

Для любого действительного числа b множество {b} тождественно равно пересечению замкнутых отрезков Icc(b − r, b + r) по всем положительным r.

LaTeX

$$$\{b\} = \bigcap_{r>0} \mathrm{Icc}(b-r,b+r)$$$

Lean4

theorem singleton_eq_inter_Icc (b : ℝ) : { b } = ⋂ (r > 0), Icc (b - r) (b + r) := by
  simp [Icc_eq_closedBall, biInter_basis_nhds Metric.nhds_basis_closedBall]

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