closedBall_eq_univ_of_half_period_le

English

If ε is at least half the period, then the closed ball around any x in AddCircle(p) of radius ε is the entire space AddCircle(p) (provided p ≠ 0).

Русский

Если радиус ε не меньше половины периода, то окружность с центром x и радиусом ε покрывает все пространство AddCircle(p) (при p ≠ 0).

LaTeX

$$$p \\neq 0 \\land \\frac{|p|}{2} \\le \\varepsilon \\Rightarrow \\mathrm{closedBall}(x, \\varepsilon) = \\mathrm{univ}$$$

Lean4

theorem closedBall_eq_univ_of_half_period_le (hp : p ≠ 0) (x : AddCircle p) {ε : ℝ} (hε : |p| / 2 ≤ ε) :
    closedBall x ε = univ :=
  eq_univ_iff_forall.mpr fun x => by simpa only [mem_closedBall, dist_eq_norm] using (norm_le_half_period p hp).trans hε

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