Theorems · Definition · combinatorics
Cycle.Chain
{α : Type u_1} → (α → α → Prop) → Cycle α → Propchain R s means that R holds between adjacent elements of s.
chain R ([a, b, c] : Cycle α) ↔ R a b ∧ R b c ∧ R c a
- Defined in
- Mathlib.Data.List.Cycle
- Cited by
- 15 results in Mathlib
- Foundations
- Depth 63 from the axioms · uses propext, Classical.choice, Quot.sound
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.
- Cyclestatement and proof · cited by 79
- Quotient.liftOn'proof · cited by 19
Cited by15
Results whose statement or proof uses this declaration.
- Cycle.chain_coe_consstatement · cited by 6
- Cycle.Chain.impstatement and proof · cited by 2
- Cycle.chain_iff_pairwisestatement and proof · cited by 2
- Function.periodicOrbit_chainstatement and proof · cited by 1
- Cycle.Chain.eq_nil_of_irreflstatement and proof · cited by 1
- Cycle.Chain.nilstatement · cited by 1
- Cycle.chain_mapstatement and proof · cited by 1
- Cycle.chain_of_pairwisestatement and proof · cited by 1
- Cycle.chain_range_succstatement and proof · cited by 1
- Cycle.forall_eq_of_chainstatement and proof · cited by 0
- Function.periodicOrbit_chain'statement · cited by 0
- Cycle.Chain.eq_nil_of_well_foundedstatement and proof · cited by 0