lean_workbook_plus_28014
ProvedIf , then and or .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_28014 (z : ℝ) (hz: 0 ≤ z ∧ z ≤ 1) : z ≥ z^2 ∧ (z = z^2 ↔ z = 0 ∨ z = 1) := by sorry
Source
If , then and or .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_28014 (z : ℝ) (hz: 0 ≤ z ∧ z ≤ 1) : z ≥ z^2 ∧ (z = z^2 ↔ z = 0 ∨ z = 1) := by sorry