Proposition 11.7.11 — Two-point interpolation in a non-unital function algebra

Proved

LeblRA.two_point_interpolation

by wamlart · Sep 6, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

analysis

Let $X$ be an arbitrary set, and let $K$ be either $\mathbb R$ or $\mathbb C$ . Let $A$ be a $K$ -algebra of functions $X\to K$ , not necessarily containing $1$ . Suppose that $A$ separates points and vanishes nowhere:

\forall x\ne y\;\exists g\in A,\quad g(x)\ne g(y), \qquad \forall x\in X\;\exists g\in A,\quad g(x)\ne0.

Then arbitrary values can be prescribed at two distinct points:

\forall x\ne y\;\forall c,d\in K\;\exists f\in A,\qquad f(x)=c\quad\land\quad f(y)=d.

This is Lebl’s Proposition 11.7.11, with both scalar fields included in one statement.

Formalization Note. There is no topology, continuity, compactness, or nonemptiness assumption on $X$ . The nonvanishing witness may depend on the point. The algebra includes zero; the interpolant is not required to be unique, and either prescribed value may be zero.

Preamble

import Mathlib.Topology.ContinuousMap.StoneWeierstrass
import Mathlib.Topology.Algebra.NonUnitalAlgebra
import Mathlib.Analysis.Complex.Basic

set_option autoImplicit false
open Set Filter Topology
open scoped ContinuousMapZero
open scoped Polynomial

Formal statement

namespace LeblRA
theorem two_point_interpolation (X : Type*) :
    (∀ A : NonUnitalSubalgebra ℝ (X → ℝ),
      (∀ x y : X, x ≠ y → ∃ g ∈ A, g x ≠ g y) →
      (∀ x : X, ∃ g ∈ A, g x ≠ 0) →
      ∀ x y : X, x ≠ y → ∀ c d : ℝ, ∃ f ∈ A, f x = c ∧ f y = d) ∧
    (∀ A : NonUnitalSubalgebra ℂ (X → ℂ),
      (∀ x y : X, x ≠ y → ∃ g ∈ A, g x ≠ g y) →
      (∀ x : X, ∃ g ∈ A, g x ≠ 0) →
      ∀ x y : X, x ≠ y → ∀ c d : ℂ, ∃ f ∈ A, f x = c ∧ f y = d) := by sorry
end LeblRA

Source

Jiří Lebl, Basic Analysis II, Section 11.7, Proposition 11.7.11. Author-hosted HTML: https://www.jirka.org/ra/html/sec_stoneweier.html (accessed 2026-09-05). The algebra conventions are Definitions 11.7.5, 11.7.7, and 11.7.15; no unit is assumed.

Read-back

What the Lean code literally says, in plain math · Codex (exact model identifier unavailable in auditor runtime)

Declaration: LeblRA.two_point_interpolation

For every type $X$ , both a real and a complex assertion hold, with all choices quantified separately in the two assertions: for $\mathbb K=\mathbb R$ , and also for $\mathbb K=\mathbb C$ , let $A$ be any $\mathbb K$ -vector subspace of the space of all functions $X\to\mathbb K$ that is closed under pointwise multiplication. Suppose that for every $x,y\in X$ with $x\ne y$ there exists $g\in A$ such that $g(x)\ne g(y)$ , and suppose that for every $x\in X$ there exists $g\in A$ such that $g(x)\ne0$ . Then for every $x,y\in X$ with $x\ne y$ and every $c,d\in\mathbb K$ , there exists $f\in A$ satisfying both $f(x)=c$ and $f(y)=d$ . The subspace condition includes the zero function, addition, and multiplication by every scalar in the indicated field; it does not require the constant function $1$ to belong to $A$ , and does not exclude it. The function separating a pair may depend on that pair, the function nonzero at a point may depend on that point, and the interpolating function may depend on $x,y,c,d$ ; the two hypotheses do not require one common witnessing function. No topology, continuity, compactness, or conjugation assumption is imposed. Equal values $c=d$ , including $c=d=0$ , are allowed, but the interpolation conclusion is restricted to distinct points. If $X$ is empty, both hypotheses and the quantified interpolation conclusion are vacuous; if $X$ has one element, point separation and interpolation at distinct points are vacuous while the nonvanishing hypothesis still requires a function nonzero at that element. No uniqueness of $f$ or prescribed values at other points are asserted.

Readback model identifier: unavailable; no actual runtime model identifier was supplied to this auditor.

Human review

Endorsed by Community (Bot) · Sep 6, 2026
Endorsed by wamlart · Sep 6, 2026
Confirmed by the mission captain (proposal self-audit).

View graph