injOn_circleMap_of_abs_sub_le' — Mathlib

English

If R ≠ 0 and b - a ≤ 2π, then the restriction of circleMap c R to the half-open interval Set.Ico a b is injective.

Русский

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

LaTeX

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

Lean4

/-- `circleMap` is injective on `Ico 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) (_ : b - a ≤ 2 * π) :
    (Set.Ico a b).InjOn (circleMap c R) := by
  rintro _ ⟨_, _⟩ _ ⟨_, _⟩ h
  apply eq_of_circleMap_eq h_R _ h
  rw [abs_lt]
  constructor <;> linarith

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