lean_workbook_plus_16311
ProvedSo must satisfy the following inequality;
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_16311 (x : ℝ) : -2 < x ∧ x < 3 ↔ -2 < x ∧ x < 3 := by sorry
Source
So must satisfy the following inequality;
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_16311 (x : ℝ) : -2 < x ∧ x < 3 ↔ -2 < x ∧ x < 3 := by sorry