Two functional identities agree on the image
ProvedWorkbookSource.problem_14812lean-workbooksource-checked
Prove that if is a monotonous function satisfying , then for all .
Source: InternLM Lean-Workbook, record lean_workbook_14812 (Apache-2.0). The complete source proposition and explicit variable declarations are preserved.
Preamble
import Mathlib open Real Nat
Formal statement
theorem WorkbookSource.problem_14812 (f : ℝ → ℝ) (h₁ : Monotone f) (h₂ : ∀ x, f (f x) = (f x)^2) (h₃ : ∀ x, f (-f x) = (f x)^2) : ∀ x ∈ Set.range f, f x = f (-x) := by sorry
Source