lean_workbook_plus_28377

Proved

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

Let $g, h \colon \mathbb{R} \to \mathbb{R}$ both continuous at $a$ , with $g(a)=h(a) = b$ . Let $f \colon \mathbb{R} \to \mathbb{R}$ be defined by $f(x) = g(x)$ if $x \in \mathbb{Q}$ and $f(x) = h(x)$ if $x \not \in \mathbb{Q}$ . Then $f$ is continuous at $a$ (where it takes value $b$ ).

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_28377  {g h f : ℝ → ℝ} {a b : ℝ} (hg : ContinuousAt g a) (hh : ContinuousAt h a) (hg' : g a = b) (hh' : h a = b)
  (hf : ∀ x, (x ∈ Set.range ((↑) : ℚ → ℝ) ↔ f x = g x) ∧ (x ∉ Set.range ((↑) : ℚ → ℝ) ↔ f x = h x)) :
  ContinuousAt f a   :=  by sorry

Source

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

View graph