OAI/Combinatorics/GraphThreshold/GraphEncoding.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LeanBlast.SecondKahnKalai.graphEdges line 13

   Source documentation

   The non-loop edge set of an ordinary graph on Fin n.

   def graphEdges {n : ℕ} (G : SimpleGraph (Fin n)) : Finset (Edge n) := by
   …

   Mentions: OAI.LeanBlast.SecondKahnKalai.Edge

2. instance OAI.LeanBlast.SecondKahnKalai.edgeMulAction line 20

   Source documentation

   Vertex permutations act on unordered non-loop edges.

   instance edgeMulAction : MulAction (Equiv.Perm (Fin n)) (Edge n) where
   …

   Mentions: OAI.LeanBlast.SecondKahnKalai.Edge

3. theorem OAI.LeanBlast.SecondKahnKalai.edge_smul_val line 34
4. theorem OAI.LeanBlast.SecondKahnKalai.mem_graphEdges line 38
5. theorem OAI.LeanBlast.SecondKahnKalai.edgeSet_graphOfEdges line 43
6. theorem OAI.LeanBlast.SecondKahnKalai.mem_edgeSet_graphOfEdges line 53
7. theorem OAI.LeanBlast.SecondKahnKalai.graphEdges_graphOfEdges line 59
8. theorem OAI.LeanBlast.SecondKahnKalai.graphOfEdges_graphEdges line 66
9. def OAI.LeanBlast.SecondKahnKalai.graphEdgeEquiv line 76

   Source documentation

   No graphs or edge sets are omitted or multiply represented.

   def graphEdgeEquiv (n : ℕ) : Finset (Edge n) ≃ SimpleGraph (Fin n) where
   …

   Mentions: OAI.LeanBlast.SecondKahnKalai.Edge

10. theorem OAI.LeanBlast.SecondKahnKalai.graphOfEdges_smul line 82
11. theorem OAI.LeanBlast.SecondKahnKalai.graphEdges_map line 89
12. theorem OAI.LeanBlast.SecondKahnKalai.graphOfEdges_empty line 96
13. theorem OAI.LeanBlast.SecondKahnKalai.graphEdges_bot line 100
14. theorem OAI.LeanBlast.SecondKahnKalai.graphEdges_top line 106
15. theorem OAI.LeanBlast.SecondKahnKalai.graphOfEdges_univ line 112
16. theorem OAI.LeanBlast.SecondKahnKalai.graphEdges_mono line 115
17. theorem OAI.LeanBlast.SecondKahnKalai.graphOfEdges_mono line 121
18. theorem OAI.LeanBlast.SecondKahnKalai.graphOfEdges_le_iff line 127
19. def OAI.LeanBlast.SecondKahnKalai.graphEdgesEquiv line 135

    Source documentation

    Edge-set encoding preserves the ordinary unlabelled edge count.

    def graphEdgesEquiv (G : SimpleGraph (Fin n)) : ↥(graphEdges G) ≃ G.edgeSet where
    …

    Mentions: OAI.LeanBlast.SecondKahnKalai.graphEdges

20. theorem OAI.LeanBlast.SecondKahnKalai.card_graphEdges line 143
21. theorem OAI.LeanBlast.SecondKahnKalai.edgeCount_graphOfEdges line 150
22. theorem OAI.LeanBlast.SecondKahnKalai.edgeCount_eq_card_edgeFinset line 154
23. theorem OAI.LeanBlast.SecondKahnKalai.edgeCount_eq_zero_iff line 160
24. theorem OAI.LeanBlast.SecondKahnKalai.positive_copies_iff line 166