sin_eq_zero_iff_of_lt_of_lt — Mathlib

English

If −π < x < π, then sin x = 0 iff x = 0.

Русский

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

LaTeX

$$$$-\pi < x < \pi \Rightarrow (\sin x = 0 \iff x = 0)$$$$

Lean4

theorem sin_eq_zero_iff_of_lt_of_lt {x : ℝ} (hx₁ : -π < x) (hx₂ : x < π) : sin x = 0 ↔ x = 0 :=
  ⟨fun h => by
    contrapose! h
    cases h.lt_or_gt with
    | inl h0 => exact (sin_neg_of_neg_of_neg_pi_lt h0 hx₁).ne
    | inr h0 => exact (sin_pos_of_pos_of_lt_pi h0 hx₂).ne',
    fun h => by simp [h]⟩

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