lean_workbook_plus_42429

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Let $f$ be a constant function - say, $f(x)=0$ for all $x.$ Then $f^{-1}([-1,1])=\mathbb{R}$ but $f(f^{-1}([-1,1]))=f(\mathbb{R})=\{0\}.$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_42429  (f : ℝ → ℝ)
  (h₀ : ∀ x, f x = 0) :
  f⁻¹' Set.Icc (-1) 1 = Set.univ ∧ f '' Set.univ = {0}   :=  by sorry

Source