injOn_circleMap_of_abs_sub_le — Mathlib

English

If R ≠ 0 and |a - b| ≤ 2π, then the restriction of circleMap c R to the interval between a and b is injective.

Русский

Если R ≠ 0 и |a - b| ≤ 2π, ограничение circleMap c R на промежуток между a и b инъективно.

LaTeX

$$$ (Ι a b).InjOn (circleMap c R) \quad \text{for } R \neq 0 \text{ and } |a - b| \le 2 \pi $$$

Lean4

/-- `circleMap` is injective on `Ι a b` if the distance between `a` and `b` is at most `2π`. -/
theorem injOn_circleMap_of_abs_sub_le {a b R : ℝ} {c : ℂ} (h_R : R ≠ 0) (_ : |a - b| ≤ 2 * π) :
    (Ι a b).InjOn (circleMap c R) := by
  rintro _ ⟨_, _⟩ _ ⟨_, _⟩ h
  apply eq_of_circleMap_eq h_R _ h
  rw [abs_lt]
  constructor <;> linarith [max_sub_min_eq_abs' a b]

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