lean_workbook_plus_74935

Proved

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

Prove that there is no bijection from $\mathbb R\to\mathbb R$ such that $f(x)f^{-1}(x)=1$ $\forall x\in\mathbb R$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_74935 : ¬∃ f : ℝ → ℝ, Function.Bijective f ∧ ∀ x : ℝ, f x * f⁻¹ x = 1   :=  by sorry

Source