lean_workbook_plus_16398
ProvedProve that when .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_16398 : ∀ c : ℝ, 0 < c ∧ c < 1 → c^2 + (1 - c)^2 < 1 := by sorry
Source
Prove that when .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_16398 : ∀ c : ℝ, 0 < c ∧ c < 1 → c^2 + (1 - c)^2 < 1 := by sorry