lean_workbook_plus_10372
ProvedProve that the function which is continuous on and satisfies for every is injective.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_10372 (f : ℝ → ℝ) (hf : Continuous f) (h : ∀ x, 6 * f (f x) = 2 * f x + x) : Function.Injective f := by sorry
Source