tan_nonneg_of_nonneg_of_le_pi_div_two

English

If 0 ≤ x ≤ π/2, then tan x ≥ 0.

Русский

Если 0 ≤ x ≤ π/2, то tan x ≥ 0.

LaTeX

$$$0 \\le x \\le \\frac{\\\\pi}{2} \\Rightarrow 0 \\le \\\\tan x$$$

Lean4

theorem tan_nonneg_of_nonneg_of_le_pi_div_two {x : ℝ} (h0x : 0 ≤ x) (hxp : x ≤ π / 2) : 0 ≤ tan x :=
  match lt_or_eq_of_le h0x, lt_or_eq_of_le hxp with
  | Or.inl hx0, Or.inl hxp => le_of_lt (tan_pos_of_pos_of_lt_pi_div_two hx0 hxp)
  | Or.inl _, Or.inr hxp => by simp [hxp, tan_eq_sin_div_cos]
  | Or.inr hx0, _ => by simp [hx0.symm]

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