Theorems · Theorem · combinatorics
SimpleGraph.Subgraph.le_induce_top_verts
∀ {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph}, G' ≤ ⊤.induce G'.verts- Cited by
- 4 results in Mathlib
- Foundations
- Depth 68 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Top.topstatement · cited by 9,680
- SimpleGraphstatement and proof · cited by 3,072
- le_topproof · cited by 411
- SimpleGraph.Subgraphstatement and proof · cited by 326
- SimpleGraph.Subgraph.vertsstatement · cited by 210
- SimpleGraph.Subgraph.inducestatement · cited by 33
- SimpleGraph.Subgraph.induce_self_vertsproof · cited by 2
- SimpleGraph.Subgraph.induce_mono_leftproof · cited by 1
Cited by4
Results whose statement or proof uses this declaration.
- SimpleGraph.Subgraph.Connected.induce_vertsproof · cited by 1
- SimpleGraph.ConnectedComponent.maximal_connected_toSubgraphproof · cited by 1
- SimpleGraph.Walk.toSubgraph_le_induce_supportproof · cited by 0
- SimpleGraph.ConnectedComponent.maximal_subgraph_connected_iffproof · cited by 0