OAI/Combinatorics/ThinTrees/Restriction.lean
13 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.StrongThinTree.MultiGraph.edgeEmbeddingline 12 - def
OAI.StrongThinTree.MultiGraph.restrictline 14 - def
OAI.StrongThinTree.MultiGraph.liftEdgesline 18 - def
OAI.StrongThinTree.MultiGraph.lowerEdgesline 20 - lemma
OAI.StrongThinTree.MultiGraph.embedding_memline 23 - lemma
OAI.StrongThinTree.MultiGraph.embedding_surjline 25 - lemma
OAI.StrongThinTree.MultiGraph.lift_univline 30 - lemma
OAI.StrongThinTree.MultiGraph.lift_lowerline 34 - lemma
OAI.StrongThinTree.MultiGraph.restrict_cutline 40 - lemma
OAI.StrongThinTree.MultiGraph.restrict_cut_cardline 49 - lemma
OAI.StrongThinTree.MultiGraph.restrict_connectedline 53 - lemma
OAI.StrongThinTree.MultiGraph.restrict_spanningTreeline 63 - lemma
OAI.StrongThinTree.MultiGraph.restrict_packableline 79