Erdős problem 907
Let be such that is continuous for every . Is it true that for some continuous and additive (i.e. )?
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/907.leanTrue ↔ ∀ (f : ℝ → ℝ), (∀ (h : ℝ), 0 < h → Continuous fun x => f (x + h) - f x) → ∃ g a, Continuous g ∧ (∀ (x y : ℝ), a (x + y) = a x + a y) ∧ f = g + aProof manifests naming this Problem
- Jayyhk Erdős Lean
jayyhk:erdos:907 - PLBY Lean proofs
ErdosProblems.Erdos907
Reported activity
Work these sources record against this Problem. Source-reported attribution, not reviewed here.
Formalization
- Machine