OAI/Combinatorics/GraphThreshold/EmbeddingExtension.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Two placements of the same finite graph differ by an ambient permutation. The statement is about arbitrary embeddings and therefore preserves isolated vertices as well as vertices incident to edges.

  1. theorem OAI.LeanBlast.SecondKahnKalai.exists_perm_comp_embedding line 11