LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6.1-sol)

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.

Closed target constraints survive compact extraction

Statement

Assume Countable and Dependent Choice. Let $X$ be a normed space with compact continuous inclusion $J : X ↪ L^{p} (Ω)$ , $1 \leq p < \infty$ , and let $C \subseteq L^{p} (Ω)$ be closed in norm. Every bounded sequence $u_{j} \in X$ with $J u_{j} \in C$ admits a subsequence $J u_{j_{k}} \to v$ in $L^{p} (Ω)$ with $v \in C$ . In particular this applies to any of this page's Rellich inclusions, with their stated domain, exponent and choice hypotheses. This statement does not assert that $v$ belongs to $X$ or that $C$ is weakly closed.

Facts & Assumptions

Given: Countable and Dependent Choice, a normed space $X$ with compact continuous inclusion $J : X ↪ L^{p} (Ω)$ , a norm-closed set $C \subseteq L^{p} (Ω)$ , and a bounded sequence $(u_{j})$ in $X$ with $J u_{j} \in C$ for all $j$ .

[F1]

The sequential form of a compact embedding. Under Countable and Dependent Choice, a compact continuous inclusion $J$ sends every bounded sequence in $X$ to a sequence with a subsequence converging in $L^{p} (Ω)$ . (Compactly embedded normed spaces)

[F2]

Closed sets contain sequential limits. A closed subset of a metric space contains the limit of every convergent sequence of its points: otherwise the open complement contains a ball about the limit, contradicting eventual membership of the sequence in that ball. (The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement, Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison, The closure of a nonempty $A$ is ${x : d (x, A) = 0}$ , equals $A$ together with its limit points, and is the smallest closed superset)

Proof

technique · extract a convergent subsequence by compactness and use closedness of the target constraint

1.1F1given

By [F1] the bounded sequence $(J u_{j})$ has a subsequence $(J u_{j_{k}})$ converging in $L^{p} (Ω)$ to some $v$ .

2.1F2step 1.1given∎

Since $J u_{j_{k}} \in C$ for every $k$ and $C$ is closed, [F2] gives $v \in C$ ; the statement makes no claim that $v$ lies in the image of $J$ . Countable and Dependent Choice are used exactly through the compact-embedding interface [F1].

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

38 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

John K. Hunter, Notes on Partial Differential Equations, complete 242-page 2014 notes (standard reference, not scraped)