Theorems · Definition · combinatorics
SimpleGraph.Free
{α : Type u_4} → {β : Type u_5} → SimpleGraph α → SimpleGraph β → PropA.Free B means that B does not contain a copy of A.
- Defined in
- Mathlib.Combinatorics.SimpleGraph.Copy
- Cited by
- 39 results in Mathlib
- Foundations
- Depth 3 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- SimpleGraphstatement and proof · cited by 3,072
- SimpleGraph.IsContainedproof · cited by 68
Cited by41
Results whose statement or proof uses this declaration.
- SimpleGraph.extremalNumberproof · cited by 23
- SimpleGraph.zarankiewiczproof · cited by 7
- SimpleGraph.card_edgeFinset_le_extremalNumberstatement and proof · cited by 6
- SimpleGraph.extremalNumber_le_iffstatement and proof · cited by 4
- SimpleGraph.free_congrstatement · cited by 4
- SimpleGraph.extremalNumber_of_fintypeCard_eqstatement and proof · cited by 3
- SimpleGraph.antitoneOn_extremalNumber_div_choose_twoproof · cited by 3
- SimpleGraph.zarankiewicz_of_fintypeCard_eqstatement and proof · cited by 2
- SimpleGraph.extremalNumber_le_iff_of_nonnegstatement and proof · cited by 2
- SimpleGraph.isExtremal_free_iffstatement and proof · cited by 2
- SimpleGraph.isExtremal_top_free_iff_isTuranMaximalstatement and proof · cited by 2
- SimpleGraph.zarankiewicz_le_iffstatement and proof · cited by 1