lean_workbook_plus_8749
OpenIsn't that we have for
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_8749 : ∀ x : ℝ, 0 < x ∧ x ≤ π / 2 → 0 < sin x ∧ sin x ≤ 1 := by sorry
Source
Isn't that we have for
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_8749 : ∀ x : ℝ, 0 < x ∧ x ≤ π / 2 → 0 < sin x ∧ sin x ≤ 1 := by sorry