biUnion_lt_ball — Mathlib

English

The union over all radii r' < r of open balls centered at x with radius r' equals the open ball of radius r around x.

Русский

Союз всех шаров радиуса r′ < r, центрированных в x, равен открытому шару радиуса r вокруг x.

LaTeX

$$$\bigcup_{r'

Lean4

theorem biUnion_lt_ball (x : α) (r : ℝ) : ⋃ r' < r, ball x r' = ball x r :=
  by
  ext
  rw [← not_iff_not]
  simp [forall_lt_imp_le_iff_le_of_dense]

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