C.3 Using the correspondence
On this page · Permalink · Source line 40
For a proof involving a restriction or a change of representation, compare the source and target spaces before identifying two displayed formulas. For an analytic estimate, check the norm, the permitted correction space, and the operator whose adjoint is used. The declarations preserve these distinctions explicitly. A continuous linear equivalence alone is not an isometry, and a coordinate equation alone does not fix the metric of its residual.
The source contains further definitions, lemmas, and examples beyond this table. The Lean guide explains its organization and the formal treatment of the principal analytic results. Verification records retain the exact source inventories and declaration types from the accepted compilation.