| Metric | Count |
|---|
DefinitionscastPred, predAbove, succAbove, finCongr | 4 |
TheoremscastAdd_inj, castAdd_injective, castLE_castSucc, castLE_comp_castSucc, castLE_inj, castLE_injective, castLE_rfl, castLT_eq_castPred, castPred_castSucc, castPred_eq_iff_eq_castSucc, castPred_eq_zero, castPred_inj, castPred_le_castPred, castPred_le_castPred_iff, castPred_le_iff, castPred_le_pred_iff, castPred_lt_castPred, castPred_lt_castPred_iff, castPred_lt_iff, castPred_mk, castPred_ne_zero, castPred_one, castPred_succAbove, castPred_succAbove_castPred, castPred_zero, castSucc_castAdd, castSucc_castPred, castSucc_injective, castSucc_le_castSucc_iff, castSucc_le_succ, castSucc_lt_or_lt_succ, castSucc_lt_succ_iff, castSucc_ne_last, castSucc_ne_zero_of_lt, castSucc_pos', castSucc_pos_iff, castSucc_predAbove_castSucc, castSucc_pred_add_one_eq, castSucc_pred_eq_pred_castSucc, castSucc_pred_lt, castSucc_pred_lt_iff, castSucc_succAbove_castSucc, castSucc_zero', cast_eq_cast, cast_inj, cast_le_cast, cast_lt_cast, castpred_succ_le_iff, coe_castPred, coe_eq_castSucc, coe_of_injective_castLE_symm, coe_of_injective_castSucc_symm, coe_succ_lt_iff_lt, eq_castSucc_of_ne_last, eq_castSucc_or_eq_last, exists_fin_succ', exists_succAbove_eq, exists_succAbove_eq_iff, exists_succ_eq, exists_succ_eq_of_ne_zero, forall_fin_succ', le_castPred_iff, le_castSucc_pred_iff, le_of_castSucc_lt_of_succ_lt, le_pred_castSucc_iff, le_pred_iff, le_zero_iff', leftInverse_cast, lt_castPred_iff, lt_castPred_succ, lt_castPred_succ_iff, lt_pred_iff, lt_succAbove_iff_le_castSucc, lt_succAbove_iff_lt_castSucc, lt_succ_castPred, lt_succ_castPred_iff, ne_succAbove, one_pos', one_succAbove_one, one_succAbove_succ, one_succAbove_zero, predAbove_castPred_of_le, predAbove_castPred_of_lt, predAbove_castPred_self, predAbove_castSucc_of_le, predAbove_castSucc_of_lt, predAbove_castSucc_self, predAbove_last_apply, predAbove_last_castSucc, predAbove_last_of_ne_last, predAbove_of_castSucc_lt, predAbove_of_le_castSucc, predAbove_of_lt_succ, predAbove_of_succ_le, predAbove_predAbove_succAbove, predAbove_pred_of_le, predAbove_pred_of_lt, predAbove_pred_self, predAbove_right_last, predAbove_right_zero, predAbove_succAbove, predAbove_succ_of_le, predAbove_succ_of_lt, predAbove_succ_self, predAbove_surjective, predAbove_zero, predAbove_zero_of_ne_zero, predAbove_zero_succ, pred_castSucc_lt, pred_castSucc_lt_iff, pred_last, pred_le_iff, pred_lt_castPred, pred_lt_castPred_iff, pred_lt_iff, pred_one', pred_succAbove, pred_succAbove_pred, range_castLE, range_castSucc, range_succ, range_succAbove, rightInverse_cast, succAbove_castPred_of_le, succAbove_castPred_of_lt, succAbove_castPred_self, succAbove_castSucc_of_le, succAbove_castSucc_of_lt, succAbove_castSucc_self, succAbove_eq_last_iff, succAbove_eq_zero_iff, succAbove_last, succAbove_last_apply, succAbove_left_inj, succAbove_left_injective, succAbove_lt_iff_castSucc_lt, succAbove_lt_iff_succ_le, succAbove_ne, succAbove_ne_last, succAbove_ne_last_last, succAbove_ne_zero, succAbove_ne_zero_zero, succAbove_of_castSucc_lt, succAbove_of_le_castSucc, succAbove_of_lt_succ, succAbove_of_succ_le, succAbove_pos, succAbove_predAbove, succAbove_pred_of_le, succAbove_pred_of_lt, succAbove_pred_self, succAbove_right_inj, succAbove_right_injective, succAbove_succAbove_predAbove, succAbove_succAbove_succAbove_predAbove, succAbove_succ_of_le, succAbove_succ_of_lt, succAbove_succ_self, succAbove_zero, succAbove_zero_apply, succ_castAdd, succ_castPred_eq_add_one, succ_castPred_eq_castPred_succ, succ_castPred_le_iff, succ_injective, succ_le_castSucc_iff, succ_le_or_le_castSucc, succ_natAdd, succ_ne_last_iff, succ_ne_last_of_lt, succ_one_eq_two', succ_predAbove_succ, succ_predAbove_zero, succ_succAbove_one, succ_succAbove_predAbove, succ_succAbove_succ, succ_succAbove_zero, succ_zero_eq_one', zero_ne_one', zero_succAbove, finCongr_apply, finCongr_apply_coe, finCongr_apply_mk, finCongr_eq_equivCast, finCongr_refl, finCongr_symm, finCongr_symm_apply, finCongr_symm_apply_coe | 188 |
| Total | 192 |
| Name | Category | Theorems |
|---|
castPred π | CompOp | 51 mathmath: castPred_lt_iff, castpred_succ_le_iff, castPred_eq_zero, castPred_castSucc, castPred_lt_castPred_iff, castPred_inj, strictMono_castPred_comp, pred_lt_castPred_iff, succ_castPred_eq_castPred_succ, castPred_succAbove_castPred, insertNth_apply_below, succAbove_castPred_of_le, pred_lt_castPred, predAbove_succ_of_lt, castPred_le_iff, predAbove_pred_of_lt, castPred_succAbove, succ_castPred_le_iff, predAbove_castPred_of_le, rev_pred, lt_castPred_iff, predAbove_castPred_self, lt_castPred_succ_iff, coe_castPred, castPred_le_castPred, lt_succ_castPred, castPred_le_castPred_iff, castLT_eq_castPred, castPred_lt_castPred, castSucc_castPred, rev_castPred, monotone_castPred_comp, SSet.stdSimplex.Ξ΄_objMkβ_of_le, SimplexCategory.II.mem_finset_iff, predAbove_of_le_castSucc, castPred_le_pred_iff, succ_castPred_eq_add_one, SimplexCategory.Ξ΄_comp_toMkβ_of_le, castPred_one, le_castPred_iff, predAbove_last_of_ne_last, predAbove_last_apply, succAbove_castPred_self, predAbove_of_lt_succ, castPred_mk, predAbove_castPred_of_lt, lt_succ_castPred_iff, lt_castPred_succ, castPred_zero, castPred_eq_iff_eq_castSucc, succAbove_castPred_of_lt
|
predAbove π | CompOp | 54 mathmath: CategoryTheory.nerve.Ο_obj, succAbove_succAbove_predAbove, predAbove_left_monotone, predAbove_predAbove_succAbove, castSucc_predAbove_castSucc, predAbove_of_castSucc_lt, succ_predAbove_succ, removeNth_removeNth_eq_swap, predAbove_succAbove, predAbove_right_last, finSuccAboveEquiv_symm_apply_ne_last, predAbove_pred_self, succ_predAbove_zero, predAbove_castSucc_of_le, succAbove_predAbove, succ_succAbove_predAbove, predAbove_succ_of_lt, predAbove_castSucc_self, finSuccEquiv'_ne_last_apply, rev_predAbove, predAbove_pred_of_lt, predAbove_right_monotone, predAbove_zero_of_ne_zero, predAbove_zero_succ, List.Vector.eraseIdx_insertIdx', predAbove_castPred_of_le, predAbove_le_predAbove, predAbove_left_injective, predAbove_of_succ_le, SimplexCategory.II.map'_succAboveOrderEmb, predAbove_last_castSucc, removeNth_removeNth_heq_swap, predAboveOrderHom_coe, predAbove_castPred_self, predAbove_rev_left, even_succAbove_add_predAbove, predAbove_surjective, SimplexCategory.II.map'_predAbove, predAbove_rev_right, predAbove_succ_of_le, predAbove_of_le_castSucc, predAbove_left_inj, predAbove_right_zero, predAbove_last_of_ne_last, predAbove_last_apply, predAbove_pred_of_le, finSuccAboveOrderIso_symm_apply_ne_last, predAbove_of_lt_succ, predAbove_castSucc_of_lt, predAbove_castPred_of_lt, neg_one_pow_succAbove_add_predAbove, succAbove_succAbove_succAbove_predAbove, predAbove_succ_self, predAbove_zero
|
succAbove π | CompOp | 160 mathmath: cycleRange_succAbove, succAbove_last, succAbove_of_le_castSucc, partialProd_contractNth, preimage_insertNth_Icc_of_mem, insertNth_comp_succAbove, succAbove_succAbove_predAbove, nndist_insertNth_insertNth, succ_succAbove_succ, predAbove_predAbove_succAbove, succAbove_rev_right, removeNth_apply, Finset.card_insertNthEquiv_filter_piFinset, succAbove_ne_last_last, insertNth_one_right, mem_piFinset_iff_pivot_removeNth, Matrix.det_succ_row, zero_succAbove, Matrix.adjugate_fin_succ_eq_det_submatrix, strictMono_succAbove, succAbove_eq_zero_iff, succ_succAbove_zero, succAbove_castSucc_self, insertNth_le_iff, insertNth_mem_piFinset_insertNth, BoxIntegral.Box.face_mk, succAbove_last_apply, finSuccEquiv'_eq_some, one_succAbove_one, BoxIntegral.Box.face_lower, one_succAbove_zero, removeNth_removeNth_eq_swap, lt_succAbove_iff_lt_castSucc, insertNthOrderIso_symm_apply, SSet.prodStdSimplex.objEquiv_Ξ΄_apply, insertNthOrderIso_toEquiv, insertNth_apply_succAbove, succAbove_rev_left, prod_univ_succAbove, insertNth_binop, succAboveEmb_apply, predAbove_succAbove, insertNth_mul, MeasureTheory.volume_preserving_piFinSuccAbove, Matrix.submatrix_updateRow_succAbove, Matrix.det_eq_sum_column_mul_submatrix_succAbove_succAbove_det, succAbove_pred_of_lt, castPred_succAbove_castPred, MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable_of_equiv, insertNth_apply_below, succAbove_predAbove, succAbove_of_succ_le, removeNth_update_succAbove, succAbove_castPred_of_le, exists_succAbove_eq, succ_succAbove_predAbove, MultilinearMap.curryMid_apply_apply, succAbove_left_injective, castPred_succAbove, pred_succAbove_pred, contractNth_apply_of_ne, Finset.filter_piFinset_eq_map_insertNthEquiv, rev_succAbove, succAbove_left_inj, succAbove_right_injective, List.Vector.eraseIdx_insertIdx', succAbove_cycleRange, LinearMap.uncurryMid_apply, lt_succAbove_iff_le_castSucc, succAbove_eq_last_iff, ContinuousMultilinearMap.curryMidEquiv_apply, MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable', succAbove_lt_iff_succ_le, MeasureTheory.measurePreserving_piFinSuccAbove, eq_self_or_eq_succAbove, Matrix.det_succ_column, Rep.standardComplex.d_of, succAbove_succ_of_lt, ContinuousLinearMap.norm_uncurryMid, succAbove_lt_succAbove_iff, finSuccAboveOrderIso_apply, removeNth_removeNth_heq_swap, Matrix.submatrix_succAbove_det_eq_negOnePow_submatrix_succAbove_det', succAbove_lt_iff_castSucc_lt, succAbove_castSucc_of_lt, Matrix.det_succ_column_zero, one_succAbove_succ, ContinuousLinearMap.uncurryMid_apply, insertNth_apply_above, castSucc_succAbove_castSucc, succAboveOrderEmb_toEmbedding, even_succAbove_add_predAbove, CategoryTheory.nerve.Ξ΄_obj, insertNth_div, Affine.Simplex.faceOpposite_point_eq_point_succAbove, Finset.map_insertNthEquiv_filter_piFinset, insertNth_update, insertNth_last, BoxIntegral.Box.face_upper, insertNth_zero, SimplexCategory.II.map'_predAbove, MultilinearMap.curryMidLinearEquiv_apply, cycleRange_symm_succ, insertNth_mem_Icc, Matrix.det_eq_sum_row_mul_submatrix_succAbove_succAbove_det, range_succAbove, succAbove_le_succAbove_iff, ContinuousMultilinearMap.curryMid_apply, insertNthOrderIso_apply, inv_partialProd_mul_eq_contractNth, succAbove_castSucc_of_le, Matrix.submatrix_succAbove_det_eq_negOnePow_submatrix_succAbove_det, succAbove_of_castSucc_lt, finSuccAboveEquiv_apply, insertNth_add, MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable, finSuccEquiv'_succAbove, MultilinearMap.curryMidLinearEquiv_symm_apply, succAbove_of_lt_succ, sum_univ_succAbove, insertNth_zero_right, dist_insertNth_insertNth, succAbove_right_inj, ContinuousMultilinearMap.norm_map_insertNth_le, succAbove_succ_self, succAbove_zero_apply, finSuccEquiv'_symm_some, le_insertNth_iff, succ_succAbove_one, succAbove_pos, neg_partialSum_add_eq_contractNth, forall_iff_succAbove, succAbove_zero, succAbove_pred_self, succAbove_castPred_self, image_succAbove_univ, Matrix.det_succ_row_zero, succAbove_succ_of_le, succAbove_ne_zero_zero, Rep.standardComplex.d_single, coe_succAboveEmb, ContinuousLinearMap.norm_map_removeNth_le, exists_succAbove_eq_iff, succAbove_inj, succAbove_pred_of_le, Finset.orderEmbOfFin_compl_singleton_apply, exists_iff_succAbove, torusIntegral_succAbove, pred_succAbove, insertNth_sub, ContinuousMultilinearMap.norm_curryMid, Matrix.submatrix_updateCol_succAbove, neg_one_pow_succAbove_add_predAbove, succAbove_succAbove_succAbove_predAbove, partialSum_contractNth, succAbove_castPred_of_lt, ContinuousMultilinearMap.curryMidEquiv_symm_apply, succAboveOrderEmb_apply, MeasurableEquiv.piFinSuccAbove_symm_apply, MeasurableEquiv.piFinSuccAbove_apply
|