Theorems · Definition · combinatorics
SimpleGraph.Copy.isoToSubgraph
{α : Type u_4} → {β : Type u_5} → {A : SimpleGraph α} → {B : SimpleGraph β} → (f : A.Copy B) → A ≃g f.toSubgraph.coeThe isomorphism from A to its copy under f : Copy A B.
- Defined in
- Mathlib.Combinatorics.SimpleGraph.Copy
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 25 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Top.topproof · cited by 9,680
- Set.Elemstatement · cited by 7,166
- SimpleGraphstatement and proof · cited by 3,072
- SimpleGraph.Subgraph.vertsstatement · cited by 210
- SimpleGraph.Isostatement · cited by 99
- SimpleGraph.Subgraph.coestatement · cited by 89
- SimpleGraph.Copystatement and proof · cited by 49
- SimpleGraph.Iso.symmproof · cited by 34
- SimpleGraph.Iso.compproof · cited by 10
- SimpleGraph.Copy.toSubgraphstatement · cited by 4
- SimpleGraph.Copy.isoSubgraphMapproof · cited by 1
- SimpleGraph.Subgraph.topIsoproof · cited by 0
Cited by3
Results whose statement or proof uses this declaration.
- SimpleGraph.isContained_iff_exists_iso_subgraphproof · cited by 3
- SimpleGraph.Copy.range_toSubgraphproof · cited by 2
- SimpleGraph.isIndContained_iff_exists_iso_subgraphproof · cited by 2