arctan_ne_mul_pi_div_two — Mathlib

English

For every integer k, arctan x ≠ (2k+1)π/2.

Русский

Для любого целого k арктангенс не принимает значение (2k+1)π/2.

LaTeX

$$$\\\\forall k \in \\\\mathbb{Z}, \\\\arctan x \\\\\\ne \\\\frac{(2k+1)\\\\pi}{2}.$$$

Lean4

theorem arctan_ne_mul_pi_div_two : ∀ (k : ℤ), arctan x ≠ (2 * k + 1) * π / 2 :=
  by
  by_contra!
  obtain ⟨k, h⟩ := this
  obtain ⟨lb, ub⟩ := arctan_mem_Ioo x
  rw [h, neg_eq_neg_one_mul, mul_div_assoc, mul_lt_mul_iff_left₀ (by positivity)] at lb
  rw [h, ← one_mul (π / 2), mul_div_assoc, mul_lt_mul_iff_left₀ (by positivity)] at ub
  norm_cast at lb ub; change -1 < _ at lb; cutsat

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