MathlibAnnex.CStarAlgebra.CAR.rootFlag
The distinguished stage corners give a nested sequence of projections supporting the root state.
Statement
Let
Definition
At stage
Assumptions
The zero coordinate is the same distinguished coordinate used by the standard stage inclusions. The index
Conclusion
Each
Main citations
- Definition and its exact construction · Exact source
- Finite root projection · Exact source
- Finite root compression · Exact source
- Initial root projection · Exact source
- Projection property · Exact source
- State support · Exact source
- Decreasing root flag · Exact source
- Compression at later stages · Exact source
Lean source signature (exact)
noncomputable def rootFlag (n : ℕ) : Limit := ofStage n (rootProjection n)
Here rootProjection n is ofStage n is rootFlag n is rootState; the projection, order, and compression facts have their own exact declarations.
Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF
Lean realization notes
The term rank one refers to
Exact Card identity
Language: en
CARD_CONTENT_COMPLETE
Card UID: lfh:lfh-declaration-card:sha256:27e0170273342fc6efeaf3843aed281ae48f8d3bf83e8272e35334315ef432f0
Card revision: 1 · SHA-256: e0f42c4aaa7c4b27b8b71167fb72f6b0b1075f96e0c31037194b8940c4c8b8d2
Exposition revision: 1 · SHA-256: f3c5e9f442221bcc55839f30bd10708e53d3460616f2f5c42bf45970d89e4ea4
Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73
Header SHA-256: 76860a7853012d8de7f42fda789f4e2ac41427a1b84bffa47c6601b5d7019c53