lean_workbook_plus_16312
ProvedThe numbers are
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_16312 (a b c : ℚ) (h₁ : a = 8 / 4) (h₂ : b = 8 / 3) (h₃ : c = 8 / 2) : a < b ∧ b < c := by sorry
Source
The numbers are
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_16312 (a b c : ℚ) (h₁ : a = 8 / 4) (h₂ : b = 8 / 3) (h₃ : c = 8 / 2) : a < b ∧ b < c := by sorry