coe_real_preimage_closedBall_period_zero

English

When the period is zero, AddCircle(0) is isomorphic to the real line, and the preimage of a closed ball under the natural inclusion equals the corresponding real closed ball.

Русский

Если период равен нулю, AddCircle(0) эквивалентен положительной вещественной прямой, и прообраз замкнутой сферы через естественное вложение совпадает с соответствующей окружностью в ℝ.

LaTeX

$$$(\\uparrow)^{-1} \\mathrm{closedBall}(x) = \\mathrm{closedBall}(x)$ в AddCircle(0)$$

Lean4

@[simp]
theorem coe_real_preimage_closedBall_period_zero (x ε : ℝ) :
    (↑) ⁻¹' closedBall (x : AddCircle (0 : ℝ)) ε = closedBall x ε :=
  by
  ext y
  simp [dist_eq_norm, ← QuotientAddGroup.mk_sub]

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