lean_workbook_plus_80985
Proved- (and so
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_80985 (x : ℝ) (h : ⌊x + 2⌋ = 1) : x ∈ Set.Icc (-1) 0 := by sorry
Source
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_80985 (x : ℝ) (h : ⌊x + 2⌋ = 1) : x ∈ Set.Icc (-1) 0 := by sorry