Prove2Me

lean_workbook_plus_1321

Proved

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

The function f(x)f(x) is strictly decreasing; f(0)=1;f(1)=0⟹f(x)∈(0,1),  ∀x∈(0,1)⟹xn∈(0,1),  ∀n∈Nf(0)=1;f(1)=0\Longrightarrow f(x)\in(0,1),\;\forall x\in(0,1)\Longrightarrow x_n\in(0,1),\;\forall n\in\mathbb{N} .

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_1321  (f : ℝ → ℝ)
  (h₀ : StrictAnti f)
  (h₁ : f 0 = 1)
  (h₂ : f 1 = 0)
  : ∀ x ∈ Set.Ioo 0 1, 0 < f x ∧ f x < 1   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph