Mathlib Map

Theorems · Theorem · combinatorics

Sym2.ind

∀ {α : Type u_1} {f : Sym2 α → Prop}, (∀ (x y : α), f s(x, y)) → ∀ (i : Sym2 α), f i
Defined in
Mathlib.Data.Sym.Sym2
Cited by
66 results in Mathlib
Foundations
Depth 4 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

SimpleGraph.edgeSet_fromEdgeSet · cited by 17SimpleGraph.edgeSet_fromE…Sym2.inductionOn · cited by 6Sym2.inductionOnSimpleGraph.not_isDiag_of_mem_edgeSet · cited by 4SimpleGraph.not_isDiag_of…Sym2.mem_and_mem_iff · cited by 4Sym2.mem_and_mem_iffSym2.other_spec' · cited by 3Sym2.other_spec'SimpleGraph.Subgraph.edgeSet_mono · cited by 3Subgraph.edgeSet_monoSimpleGraph.Subgraph.edgeSet_subset · cited by 3Subgraph.edgeSet_subsetSym2.fromRel_bot · cited by 3Sym2.fromRel_botSym2.fromRel_irrefl · cited by 2Sym2.fromRel_irreflSimpleGraph.Hom.map_mem_edgeSet · cited by 2Hom.map_mem_edgeSetSimpleGraph.completeEquipartiteGraph_eq_bot_iff · cited by 2SimpleGraph.completeEquip…SimpleGraph.Subgraph.edgeSet_coe · cited by 2Subgraph.edgeSet_coeFinset.coe_sym2 · cited by 2Finset.coe_sym2Sym2.card_toFinset_of_not_isDiag · cited by 2Sym2.card_toFinset_of_not…SimpleGraph.Subgraph.mem_verts_of_mem_edge · cited by 2Subgraph.mem_verts_of_mem…Sym2 · cited by 737Sym2Sym2.mk · cited by 332Sym2.mkSym2.indCITED BYCITES

Cites2

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Sym2statement and proof · cited by 737
  • Sym2.mkstatement and proof · cited by 332

Cited by66

Results whose statement or proof uses this declaration.