Theorems · Definition · order theory
Fin.succAboveOrderEmb
{n : ℕ} → Fin (n + 1) → Fin n ↪o Fin (n + 1)Fin.succAbove p as an OrderEmbedding.
- Defined in
- Mathlib.Order.Fin.Basic
- Cited by
- 15 results in Mathlib
- Foundations
- Depth 29 from the axioms · uses propext
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- OrderEmbeddingstatement · cited by 619
- Fin.succAboveproof · cited by 249
- OrderEmbedding.ofStrictMonoproof · cited by 15
- Fin.strictMono_succAboveproof · cited by 8
Cited by17
Results whose statement or proof uses this declaration.
- SimplexCategory.δproof · cited by 146
- Fin.succAboveOrderEmb_applystatement and proof · cited by 10
- SimplexCategory.mkOfSucc_δ_gtproof · cited by 4
- SimplexCategory.mkOfSucc_δ_ltproof · cited by 3
- SimplexCategory.mkOfSucc_δ_eqproof · cited by 3
- SimplexCategory.rev_map_δproof · cited by 2
- Finset.orderEmbOfFin_compl_singletonstatement and proof · cited by 2
- SSet.boundary_obj_eq_univproof · cited by 1
- Finset.orderEmbOfFin_compl_singleton_applyproof · cited by 1
- SimplexCategory.II.map'_succAboveOrderEmbstatement and proof · cited by 1
- Fin.succAboveOrderIsoproof · cited by 1
- SSet.StrictSegal.spine_δ_vertex_geproof · cited by 0