OAI/Combinatorics/GraphThreshold/GraphContainment.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LeanBlast.SecondKahnKalai.card_mappedGraphEdges line 14
2. theorem OAI.LeanBlast.SecondKahnKalai.mapped_copy_le line 20
3. theorem OAI.LeanBlast.SecondKahnKalai.isContained_iff_exists_smul_subset line 28

   Source documentation

   Containment of a graph is equivalent to containing a permuted copy of its edges. The embedding carries all vertices, so isolated vertices are retained.

   theorem isContained_iff_exists_smul_subset (f : V ↪ Fin n) (H : SimpleGraph V)
       (W : Finset (Edge n)) :
       H.IsContained (graphOfEdges W) ↔
         ∃ σ : Equiv.Perm (Fin n), σ • graphEdges (H.map f) ⊆ W := by
   …

   Mentions: OAI.LeanBlast.SecondKahnKalai.Edge, OAI.LeanBlast.SecondKahnKalai.graphOfEdges, OAI.LeanBlast.SecondKahnKalai.graphEdges

4. theorem OAI.LeanBlast.SecondKahnKalai.copyCount_pos_iff_exists_smul_subset line 51
5. theorem OAI.LeanBlast.SecondKahnKalai.exists_graphRepresentation line 57