English
For any p, x, and ε, the preimage under the quotient map of the closed ball around x in AddCircle(p) equals the union over all integers z of closed balls around x + z p.
Русский
Для любого p, x и ε пределобраз под тождественным отображением квадрата взятого по p равен объединению по z∈ℤ замкнутых шаров вокруг x + z p.
LaTeX
$$$(\\uparrow)^{-1}'\\mathrm{closedBall}(x, \\varepsilon) = \\bigcup_{z \\in \\mathbb{Z}} \\mathrm{closedBall}(x + z p, \\varepsilon)$$$
Lean4
theorem coe_real_preimage_closedBall_eq_iUnion (x ε : ℝ) :
(↑) ⁻¹' closedBall (x : AddCircle p) ε = ⋃ z : ℤ, closedBall (x + z • p) ε :=
by
rcases eq_or_ne p 0 with (rfl | hp)
· simp [iUnion_const]
ext y
simp only [dist_eq_norm, mem_preimage, mem_closedBall, zsmul_eq_mul, mem_iUnion, Real.norm_eq_abs,
← QuotientAddGroup.mk_sub, norm_eq, ← sub_sub]
refine ⟨fun h => ⟨round (p⁻¹ * (y - x)), h⟩, ?_⟩
rintro ⟨n, hn⟩
rw [← mul_le_mul_iff_right₀ (abs_pos.mpr <| inv_ne_zero hp), ← abs_mul, mul_sub, mul_comm _ p,
inv_mul_cancel_left₀ hp] at hn ⊢
exact (round_le (p⁻¹ * (y - x)) n).trans hn
