Theorems · Theorem · order theory
RelSeries.eraseLast_toFun
∀ {α : Type u_1} {r : SetRel α α} (p : RelSeries r) (i : Fin (p.length - 1 + 1)), p.eraseLast.toFun i = p.toFun ⟨↑i, ⋯⟩- Defined in
- Mathlib.Order.RelSeries
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 24 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- SetRelstatement and proof · cited by 581
- RelSeries.lengthstatement and proof · cited by 195
- RelSeriesstatement and proof · cited by 129
- RelSeries.toFunstatement and proof · cited by 114
- RelSeries.eraseLaststatement and proof · cited by 21
Cited by4
Results whose statement or proof uses this declaration.
- RelSeries.eraseLast_last_rel_lastproof · cited by 4
- CompositionSeries.mem_eraseLast_of_ne_of_memproof · cited by 1
- CompositionSeries.snoc_eraseLast_lastproof · cited by 1
- RelSeries.toList_eraseLastproof · cited by 1