Proof of `Almost-embedding transfer with isolated source vertices`
groundedproofs/Lax263307Proofs/IsolatedEmbeddingTransfer.lean · lax-263307
What this proof establishes
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
Relabel the nonisolated induced subgraph by Fin and restrict the source almost-embedding along its induced embedding. Degrees cannot increase and this subgraph has no isolated vertices. Apply the proved transfer, pull the decomposition back to the induced graph, and attach singleton bags for the omitted isolated vertices using the proved tree-extension construction.