PropositionStatement: Literature-sourcedProof: AI-generatedPipeline-generated

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.

Finite-dimensional Stiefel and Grassmann manifolds are compact

Statement

For $1 \leq r \leq n$ , $St (n, r)$ is a nonempty closed bounded subset of $R^{n \times r}$ , and $Gr (r, n)$ is compact as its continuous quotient image. Hence both spaces are compact.

Facts & Assumptions

Given: Integers $1 \leq r \leq n$ and the Stiefel and quotient definitions of Real Stiefel and Grassmann optimization conventions.

[F1]

A subset of finite-dimensional Euclidean space is compact if it is closed and bounded (For a nonempty subset of $R^{n}$ with $n \geq 1$ , compactness, closedness and boundedness, pseudocompactness, and attainment of extrema by every continuous real-valued function are equivalent).

[F2]

The quotient map $q : X \mapsto [X]$ is continuous for the quotient topology and is surjective by the quotient definition in the real conventions.

Proof

technique · Heine–Borel followed by the open-cover definition of quotient compactness

1.1givenF1algebra

The equations $X^{T} X = I_{r}$ are polynomial equations in the entries, so their common zero set is closed. Also $∥ X ∥_{F}^{2} = tr (X^{T} X) = r$ , so the set is bounded. The matrix with columns $e_{1}, \dots, e_{r}$ belongs to it, so it is nonempty.

2.1F1F2step 1.1choose

Let $U$ be any open cover of $Gr (r, n)$ . By [F2], the sets $q^{- 1} (U)$ for $U \in U$ are open in $St (n, r)$ and cover it. Compactness from step 1.1 gives $U_{1}, \dots, U_{k} \in U$ whose preimages cover $St (n, r)$ . Since $q$ is surjective, $U_{1}, \dots, U_{k}$ cover $Gr (r, n)$ . Thus the quotient is compact directly from the open-cover definition.

3.1step 1.1step 2.1∎

Step 1.1 proves compactness of $St (n, r)$ and step 2.1 proves compactness of $Gr (r, n)$ , as claimed.

Depends on

Used by

Riemannian trust regions reach an epsilon-gradient iterate Theorem

Dependency tree · two levels

12 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

P.-A. Absil, R. Mahony, and R. Sepulchre, Optimization Algorithms on Matrix Manifolds, Chapter 3 (2008) (standard reference, not scraped)
Nicolas Boumal, An Introduction to Optimization on Smooth Manifolds (2023 prepublication) (standard reference, not scraped)