lean_workbook_plus_44869

Disproved

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

Let $f$ and $g$ two functions continuous in $\mathbb{R}$ , such that $f^2(x)+g^2(x)=1$ . Prove that it exists at least one solution of the equation $f(x)\cdot g(x)=1$ in the $[-1,1]$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_44869 (f g : ℝ → ℝ) (hf : Continuous f) (hg : Continuous g) (h : ∀ x, (f x)^2 + (g x)^2 = 1) : ∃ x ∈ Set.Icc (-1) 1, f x * g x = 1   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph