cos_eq_one_iff_of_lt_of_lt — Mathlib

English

If −2π < x < 2π, then cos x = 1 iff x = 0.

Русский

Если −2π < x < 2π, то cos x = 1 тогда и только тогда, когда x = 0.

LaTeX

$$$$-(2\pi) < x < 2\pi \Rightarrow \cos x = 1 \iff x = 0$$$$

Lean4

theorem cos_eq_one_iff_of_lt_of_lt {x : ℝ} (hx₁ : -(2 * π) < x) (hx₂ : x < 2 * π) : cos x = 1 ↔ x = 0 :=
  ⟨fun h => by
    rcases (cos_eq_one_iff _).1 h with ⟨n, rfl⟩
    rw [mul_lt_iff_lt_one_left two_pi_pos] at hx₂
    rw [neg_lt, neg_mul_eq_neg_mul, mul_lt_iff_lt_one_left two_pi_pos] at hx₁
    norm_cast at hx₁ hx₂
    obtain rfl : n = 0 := le_antisymm (by cutsat) (by cutsat)
    simp, fun h => by simp [h]⟩

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