GraphSupport.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

def OAI.LeanBlast.SecondKahnKalai.edgeSubgraph line 15
Source documentation
The subgraph containing exactly the given edges and their incident vertices. For the empty edge set this has no vertices, as required for internal copies.
```
def edgeSubgraph (S : Finset (Edge n)) : (⊤ : SimpleGraph (Fin n)).Subgraph where
…
```
Mentions: OAI.LeanBlast.SecondKahnKalai.Edge
def OAI.LeanBlast.SecondKahnKalai.edgeSupportGraph line 22
theorem OAI.LeanBlast.SecondKahnKalai.edgeSubgraph_spanningCoe line 26
theorem OAI.LeanBlast.SecondKahnKalai.edgeSupportGraph_map line 30
theorem OAI.LeanBlast.SecondKahnKalai.edgeSupportGraph_noIsolates line 35

def OAI.LeanBlast.SecondKahnKalai.supportIso line 43

Source documentation

Restriction of a graph isomorphism to its incident vertices.

def supportIso {V W : Type*} {G : SimpleGraph V} {H : SimpleGraph W}
    (e : G ≃g H) : G.induce G.support ≃g H.induce H.support where
…

def OAI.LeanBlast.SecondKahnKalai.edgeSupportGraph_smulIso line 55
theorem OAI.LeanBlast.SecondKahnKalai.map_eq_of_iso line 62
theorem OAI.LeanBlast.SecondKahnKalai.exists_smul_eq_of_edgeSupportGraph_iso line 75
Source documentation
An isomorphism of incident-vertex graphs extends to a permutation of the full ambient vertex set, hence to equality of the corresponding edge copies.
```
theorem exists_smul_eq_of_edgeSupportGraph_iso {S T : Finset (Edge n)}
    (e : edgeSupportGraph S ≃g edgeSupportGraph T) :
    ∃ σ : Equiv.Perm (Fin n), σ • S = T := by
…
```
Mentions: OAI.LeanBlast.SecondKahnKalai.Edge, OAI.LeanBlast.SecondKahnKalai.edgeSupportGraph
theorem OAI.LeanBlast.SecondKahnKalai.subgraph_eq_edgeSubgraph line 95
theorem OAI.LeanBlast.SecondKahnKalai.subgraph_eq_edgeSubgraph_of_iso line 113
theorem OAI.LeanBlast.SecondKahnKalai.edgeCount_edgeSupportGraph line 124
def OAI.LeanBlast.SecondKahnKalai.edgeSupportGraph_copy_of_subset line 134
Source documentation
A selected edge subset of an embedded graph pulls back to an actual copy inside the original graph, using only incident vertices of the selection.
```
def edgeSupportGraph_copy_of_subset {V : Type*} (f : V ↪ Fin n)
    (H : SimpleGraph V) (S : Finset (Edge n))
    (hS : S ⊆ graphEdges (H.map f)) : (edgeSupportGraph S).Copy H := by
…
```
Mentions: OAI.LeanBlast.SecondKahnKalai.Edge, OAI.LeanBlast.SecondKahnKalai.graphEdges, OAI.LeanBlast.SecondKahnKalai.edgeSupportGraph
theorem OAI.LeanBlast.SecondKahnKalai.exists_subgraph_iso_edgeSupportGraph line 156