lean_workbook_plus_32500

Open

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

For $f(x)=\frac{9^x}{9^x+3}$ $\implies{f(x)+f(1-x)=1}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_32500  (x : ℝ)
  (f : ℝ → ℝ)
  (h₀ : ∀ x, f x = 9^x / (9^x + 3))
  (h₁ : 0 < x)
  (h₂ : x < 1) :
  f x + f (1 - x) = 1   :=  by sorry

Source

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

View graph