preimage_circleMap — Mathlib

English

If s ⊆ ℂ is countable, then (circleMap c R)^{-1}(s) is countable provided R ≠ 0.

Русский

Если s ⊆ ℂ счётно, то (circleMap c R)^{-1}(s) счётно при условии R ≠ 0.

LaTeX

$$$ s.Countable \Rightarrow (circleMap c R)^{-1}(s) \text{ is countable} \quad \text{and} \; R \neq 0 $$$

Lean4

theorem preimage_circleMap {s : Set ℂ} (hs : s.Countable) (c : ℂ) {R : ℝ} (hR : R ≠ 0) :
    (circleMap c R ⁻¹' s).Countable :=
  show (((↑) : ℝ → ℂ) ⁻¹' ((· * I) ⁻¹' (exp ⁻¹' ((R * ·) ⁻¹' ((c + ·) ⁻¹' s))))).Countable from
    (((hs.preimage (add_right_injective _)).preimage <|
              mul_right_injective₀ <| ofReal_ne_zero.2 hR).preimage_cexp.preimage <|
          mul_left_injective₀ I_ne_zero).preimage
      ofReal_injective

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