lean_workbook_plus_14271
Proved- for all , or for all .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_14271 (f : ℝ → ℝ) (hf: f = id ∨ f = abs) : ∀ x, f x = x ∨ ∀ x, f x = |x| := by sorry
Source
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_14271 (f : ℝ → ℝ) (hf: f = id ∨ f = abs) : ∀ x, f x = x ∨ ∀ x, f x = |x| := by sorry