Proof of `Nonempty raw frame spaces` (2nd statement)
groundedproofs/Lax342547Proofs/FrameExistence.lean · lax-342547
What this proof establishes
no assumptions
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
Description
Pad the explicit doubled frame with zero rows and transport it across a coordinate equivalence to any ambient space of dimension at least 2(d+h).