lean_workbook_plus_40592

Proved

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

Given $0 < x < 1$ , if $f(x) \geq 1 - x^n$ holds for all $n \in \mathbb{N}$ , can we conclude that $f(x) \geq 1$ ?

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_40592 (x : ℝ) (n : ℕ) (f : ℝ → ℝ) (hf: 0 < x ∧ x < 1) (h: ∀ n : ℕ, f x >= 1 - x ^ n): f x >= 1   :=  by sorry

Source