Mathlib Map

Theorems · Definition · order theory

Fin.predAbove

{n : ℕ} → Fin n → Fin (n + 1) → Fin n

predAbove p i surjects i : Fin (n+1) into Fin n by subtracting one if p < i.

Defined in
Mathlib.Data.Fin.SuccPred
Cited by
75 results in Mathlib
Foundations
Depth 28 from the axioms · uses propext
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Fin.predAbove_of_le_castSucc · cited by 24Fin.predAbove_of_le_castS…Fin.predAbove_of_castSucc_lt · cited by 22Fin.predAbove_of_castSucc…SSet.prodStdSimplex.pairingCore.IsType₂.φ · cited by 14IsType₂.φFin.predAbove_succ_of_le · cited by 5Fin.predAbove_succ_of_leSimplexCategory.δ_comp_σ_of_gt · cited by 5SimplexCategory.δ_comp_σ_…SimplexCategory.δ_comp_σ_of_le · cited by 5SimplexCategory.δ_comp_σ_…SimplexCategory.coe_σ · cited by 4SimplexCategory.coe_σSSet.prodStdSimplex.pairingCore.IsType₂.φ_succAbove · cited by 4IsType₂.φ_succAboveFin.predAbove_castSucc_of_le · cited by 4Fin.predAbove_castSucc_of…Fin.predAbove_right_last · cited by 4Fin.predAbove_right_lastFin.predAbove_zero_of_ne_zero · cited by 4Fin.predAbove_zero_of_ne_…SimplexCategory.σ_comp_σ · cited by 4SimplexCategory.σ_comp_σSSet.prodStdSimplex.pairingCore.IsType₂.φ_castSucc · cited by 3IsType₂.φ_castSuccSSet.prodStdSimplex.pairingCore.IsType₂.φ_of_ne · cited by 3IsType₂.φ_of_neFin.succAbove_predAbove · cited by 3Fin.succAbove_predAboveFin.castPred · cited by 89Fin.castPredFin.predAboveCITED BYCITES

Cites1

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

Cited by79

Results whose statement or proof uses this declaration.