lean_workbook_plus_4142

Proved

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

Let $(E,d)$ be a metric space. Let $f:E\to\mathbb R$ be a function such that for all $a\in\mathbb R$ the sets $X=\{x\in E:f(x)<a\}$ and $Y=\{x\in E:f(x)>a\}$ are open in $E.$ Show that $f$ is continuous.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_4142 (E : Type*) [MetricSpace E] (f : E → ℝ)
    (hf : ∀ a : ℝ, IsOpen {x | f x < a} ∧ IsOpen {x | f x > a}) :
    Continuous f   :=  by sorry

Source

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

View graph