LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Riesz lemma

Statement

Let $X$ be a normed space, let $M ⊊ X$ be a proper closed normed subspace (Normed subspace), and let $0 < α < 1$ . Then there exists $x \in X$ such that $∥ x ∥ = 1$ and

$dist (x, M) : = \inf_{m \in M} ∥ x - m ∥ > α .$

Facts & Assumptions

Given: A normed space $X$ , a proper closed normed subspace $M ⊊ X$ , and a real $α$ with $0 < α < 1$ .

[A1]

The subspace $M$ is proper and closed in $X$ .

Proof

technique · direct

1.1

By [A1], choose $y \in X ∖ M$ and put $d : = \inf_{m \in M} ∥ y - m ∥$ . Because $M$ is closed, its complement is open, so there is $ρ > 0$ with $B (y, ρ) \subseteq X ∖ M$ . Hence $∥ y - m ∥ \geq ρ$ for every $m \in M$ , which gives $d \geq ρ > 0$ .

A1choosealgebra

2.1

Since $α < 1$ , one has $d < d / α$ . By definition of the infimum, choose $m \in M$ with $d \leq ∥ y - m ∥ < \frac{d}{α} .$ Put $x : = \frac{y - m}{∥ y - m ∥} .$ Then $∥ x ∥ = 1$ .

step 1.1choosealgebra

3.1

Let $m^{'} \in M$ . Because $m + ∥ y - m ∥ m^{'} \in M$ , the definition of $d$ gives $d \leq ∥ y - (m + ∥ y - m ∥ m^{'}) ∥ = ∥ y - m - ∥ y - m ∥ m^{'} ∥ = ∥ y - m ∥ ∥ x - m^{'} ∥ .$ Therefore $∥ x - m^{'} ∥ \geq \frac{d}{∥ y - m ∥} > α,$ the last inequality by step 2.1. Since $m^{'} \in M$ was arbitrary, $dist (x, M) > α$ .

step 2.1givenalgebra

4.1

Step 3.1 produces a unit vector $x$ whose distance from $M$ exceeds $α$ , as required.

step 2.1step 3.1∎

Remarks

The proof uses only an approximate minimizer. No nearest-point theorem is assumed.

Depends on

Normed subspace

Used by

Dependency tree · two levels

4 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Tomasz Kochanek, Functional analysis, Lecture 1 (standard reference, not scraped)
Gerald Teschl, Topics in Real and Functional Analysis (standard reference, not scraped)
Paul Howard and Eleftherios Tachtsis, On infinite-dimensional Banach spaces and weak forms of the axiom of choice (standard reference, not scraped)