circleMap_preimage_codiscrete — Mathlib

English

For R ≠ 0, the pushforward of codiscrete Real under circleMap is contained in codiscreteWithin(Sphere(c, |R|)).

Русский

Если R ≠ 0, то образ кодискретного Real через circleMap лежит в codiscreteWithin(Sphere(c, |R|)).

LaTeX

$$$\text{map}(circleMap(c,R))\big(\text{codiscrete}(\mathbb{R})\big) \le \text{codiscreteWithin}(\mathbb{S}(c,|R|)).$$$

Lean4

theorem circleMap_preimage_codiscrete {c : ℂ} {R : ℝ} (hR : R ≠ 0) :
    map (circleMap c R) (codiscrete ℝ) ≤ codiscreteWithin (Metric.sphere c |R|) :=
  by
  intro s hs
  apply (analyticOnNhd_circleMap c R).preimage_mem_codiscreteWithin
  · intro x hx
    by_contra hCon
    obtain ⟨a, ha⟩ := eventuallyConst_iff_exists_eventuallyEq.1 hCon
    have := ha.deriv.eq_of_nhds
    simp [hR] at this
  · rwa [Set.image_univ, range_circleMap]

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