| Metric | Count |
|---|
Definitionsappend, cons, consCases, consEquiv, consInduction, contractNth, find, init, insertNth, insertNthEquiv, removeNth, repeat, snoc, snocCases, snocEquiv, snocInduction, succAboveCases, tail, piFinTwoEquiv | 19 |
TheoremsaddCases_castAdd_natAdd, append_assoc, append_castAdd_natAdd, append_cast_left, append_cast_right, append_comp_rev, append_comp_sumElim, append_cons, append_elim0, append_injective_iff, append_left, append_left', append_left_eq_cons, append_left_nil, append_left_snoc, append_rev, append_right, append_right_cons, append_right_eq_snoc, append_right_nil, append_snoc, comp_cons, comp_contractNth, comp_init, comp_snoc, comp_tail, consCases_cons, consEquiv_apply, consEquiv_symm_apply, cons_comp_rev, cons_eq_append, cons_inj, cons_injective2, cons_injective_iff, cons_injective_of_injective, cons_last, cons_le, cons_le_cons, cons_left_injective, cons_one, cons_rev, cons_right_injective, cons_self_tail, cons_snoc_eq_snoc_cons, cons_succ, cons_update, cons_zero, contractNth_apply_of_eq, contractNth_apply_of_gt, contractNth_apply_of_lt, contractNth_apply_of_ne, elim0_append, eq_insertNth_iff, eq_self_or_eq_succAbove, exists_cons, exists_fin_succ_pi, exists_fin_zero_pi, exists_iff_castSucc, exists_iff_succ, exists_iff_succAbove, find?_decide_eq_dite, find?_decide_get_eq_find, find?_eq_dite, find?_eq_some_find_of_exists, find?_eq_some_find_of_isSome, find_congr, find_congr', find_eq_dite, find_eq_iff, find_eq_zero, find_le, find_le_iff, find_le_of_pos, find_lt_iff, find_mem_find?_decide, find_min, find_mono, find_mono_of_le, find_nat_lt, find_of_find_le, find_of_not_zero, find_pos, find_spec, forall_fin_add, forall_fin_add_pi, forall_fin_succ_pi, forall_fin_zero_pi, forall_iff_castSucc, forall_iff_succ, forall_iff_succAbove, get_find?_eq_find_of_eq_true, init_def, init_snoc, init_update_castSucc, init_update_last, insertNthEquiv_apply, insertNthEquiv_last, insertNthEquiv_symm_apply, insertNthEquiv_zero, insertNth_apply_above, insertNth_apply_below, insertNth_apply_same, insertNth_apply_succAbove, insertNth_binop, insertNth_comp_rev, insertNth_comp_succAbove, insertNth_eq_iff, insertNth_inj, insertNth_injective2, insertNth_last, insertNth_last', insertNth_le_iff, insertNth_left_injective, insertNth_removeNth, insertNth_rev, insertNth_right_injective, insertNth_self_removeNth, insertNth_succ_cons, insertNth_update, insertNth_zero, insertNth_zero', le_cons, le_find_iff, le_insertNth_iff, lt_find_iff, mem_find?_iff, range_cons, range_fin_succ, range_snoc, removeNth_apply, removeNth_fun_const, removeNth_insertNth, removeNth_last, removeNth_removeNth_eq_swap, removeNth_removeNth_heq_swap, removeNth_update, removeNth_update_succAbove, removeNth_zero, repeat_add, repeat_apply, repeat_comp_rev, repeat_one, repeat_rev, repeat_succ, repeat_zero, sigma_eq_iff_eq_comp_cast, sigma_eq_of_eq_comp_cast, snocCases_snoc, snocEquiv_apply, snocEquiv_symm_apply, snoc_apply_zero, snoc_castAdd, snoc_castSucc, snoc_comp_castAdd, snoc_comp_castSucc, snoc_comp_natAdd, snoc_comp_rev, snoc_eq_append, snoc_init_self, snoc_inj, snoc_injective2, snoc_injective_iff, snoc_injective_of_injective, snoc_last, snoc_left_injective, snoc_rev, snoc_right_injective, snoc_update, snoc_zero, succAbove_cases_eq_insertNth, tail_cons, tail_def, tail_init_eq_init_tail, tail_update_succ, tail_update_zero, tuple0_le, update_cons_zero, update_insertNth, update_snoc_last, val_find, piFinTwoEquiv_apply, piFinTwoEquiv_symm_apply | 182 |
| Total | 201 |
| Name | Category | Theorems |
|---|
append 📖 | CompOp | 38 mathmath: append_right_cons, appendHomeomorph_apply, append_elim0, append_assoc, List.ofFn_fin_append, append_left_eq_cons, appendIsometryOfEq_apply, append_right_nil, elim0_append, append_left_snoc, append_right_eq_snoc, Embedding.coe_append, TensorPower.tprod_mul_tprod, append_right, append_cons, append_comp_sumElim, cons_eq_append, append_snoc, append_injective_iff, succFunEquiv_symm_apply, append_left', repeat_add, take_append_left, snoc_eq_append, append_left, append_cast_right, repeat_succ, append_rev, append_cast_left, append_castAdd_natAdd, append_comp_rev, appendIsometry_apply, continuous_append, take_append_right, appendEquiv_apply, edist_append_eq_max_edist, append_left_nil, RelSeries.append_toFun
|
cons 📖 | CompOp | 130 mathmath: ContinuousAlternatingMap.cons_add, differentiableWithinAt_finCons', insertNth_succ_cons, DifferentiableAt.finCons, cons_inj, DifferentiableWithinAt.finCons, Embedding.coe_cons, cons_injective_of_injective, HasStrictFDerivAt.finCons, cons_succ, ContinuousOn.finCons, Module.Basis.coe_mkFinConsOfLE, LinearEquiv.piFinTwo_symm_apply, torusIntegral_succ, consEquiv_apply, append_right_cons, MeasurableEquiv.piFinTwo_symm_apply, HasDerivAt.finCons, differentiable_finCons', exists_linearIndependent_cons_of_lt_finrank, Function.FromTypes.uncurry_apply_cons, Matrix.vandermonde_succ, consEquivL_apply, consCases_cons, Differentiable.finCons, preimage_apply_01_prod, hasFDerivAt_finCons, hasFDerivWithinAt_finCons, Function.FromTypes.curry_apply_succ, exists_linearIndependent_cons_of_lt_rank, MvPolynomial.eval_eq_eval_mv_eval', exists_cons, differentiableOn_finCons', linearIndependent_fin_cons, append_left_eq_cons, ContinuousMultilinearMap.cons_smul, sum_cons, hasFDerivWithinAt_finCons', exists_fin_succ_pi, append_left_snoc, hasStrictFDerivAt_finCons, cons_comp_rev, cons_le_cons, snoc_eq_cons_rotate, cons_last, ContinuousMultilinearMap.cons_add, hasFDerivAt_finCons', HasFDerivAt.finCons, cons_snoc_eq_snoc_cons, cons_apply_cycleRange, hasStrictDerivAt_finCons', hasStrictDerivAt_finCons, update_cons_zero, append_cons, HasFDerivWithinAt.finCons, differentiableAt_finCons, cons_one, OrderedFinpartition.extendLeft_partSize, cons_le, Continuous.finCons, ContinuousWithinAt.finCons, IsometryEquiv.piFinTwo_symm_apply, cons_self_tail, MultilinearMap.cons_add, cons_eq_append, consOrderIso_apply, MultilinearMap.curryLeft_apply, insertNth_zero', cons_left_injective, MultilinearMap.cons_smul, LinearIndependent.fin_cons, ContinuousAlternatingMap.cons_smul, hasStrictFDerivAt_finCons', prodEquivPiFinTwo_apply, Matrix.vandermonde_cons, FirstOrder.Language.Formula.realize_graph, hasDerivAtFilter_finCons', hasDerivWithinAt_finCons', range_cons, hasFDerivAtFilter_finCons, continuousMultilinearCurryLeftEquiv_apply, LinearIndependent.fin_cons', pi_lex_lt_cons_cons, insertNth_zero, snoc_eq_append, prodEquivPiFinTwo_symm_apply, Equiv.coe_embeddingFinSucc_symm, differentiableAt_finCons', MeasurableEquiv.finTwoArrow_symm_apply, insertNth_comp_cycleRange_symm, HasStrictDerivAt.finCons, cons_mem_piFinset_cons, hasDerivAtFilter_finCons, forall_fin_succ_pi, cons_injective_iff, comp_cons, ContinuousMultilinearMap.curryLeft_apply, snoc_rev, hasDerivAt_finCons', cons_injective2, DifferentiableOn.finCons, ContinuousAt.finCons, le_cons, HasDerivAtFilter.finCons, hasFDerivAtFilter_finCons', HasFDerivAtFilter.finCons, Module.Basis.coe_mkFinCons, ContinuousMultilinearMap.norm_map_cons_le, cons_right_injective, differentiable_finCons, differentiableOn_finCons, hasDerivWithinAt_finCons, UniformEquiv.piFinTwo_symm_apply, Homeomorph.piFinTwo_symm_apply, piFinTwoEquiv_symm_apply, prod_cons, cons_comp_cycleRange, Filter.Tendsto.finCons, cons_update, hasDerivAt_finCons, ContinuousLinearEquiv.piFinTwo_symm_apply, snoc_comp_rev, List.ofFn_cons, cons_zero, Function.FromTypes.curry_apply_cons, HasDerivWithinAt.finCons, differentiableWithinAt_finCons, insertNth_apply_cycleRange_symm, tail_cons, cons_rev
|
consCases 📖 | CompOp | 1 mathmath: consCases_cons
|
consEquiv 📖 | CompOp | 10 mathmath: Action.diagonalSuccIsoTensorDiagonal_inv_hom, Finset.map_consEquiv_filter_piFinset, consEquiv_apply, insertNthEquiv_zero, Finset.filter_piFinset_eq_map_consEquiv, consEquiv_symm_apply, consOrderIso_toEquiv, Action.diagonalSuccIsoTensorDiagonal_hom_hom, consLinearEquiv_symm_apply, consLinearEquiv_apply
|
consInduction 📖 | CompOp | — |
contractNth 📖 | CompOp | 12 mathmath: partialProd_contractNth, contractNth_apply_of_gt, contractNth_apply_of_ne, groupHomology.inhomogeneousChains.d_single, inhomogeneousCochains.d_hom_apply, inv_partialProd_mul_eq_contractNth, neg_partialSum_add_eq_contractNth, contractNth_apply_of_eq, Rep.barComplex.d_single, comp_contractNth, partialSum_contractNth, contractNth_apply_of_lt
|
find 📖 | CompOp | 25 mathmath: find_eq_iff, find_pos, find_congr', find_eq_zero, find_mono_of_le, find?_eq_dite, find_le_iff, le_find_iff, find?_eq_some_find_of_isSome, find_le_of_pos, find_spec, find_congr, find_mono, lt_find_iff, find?_eq_some_find_of_exists, get_find?_eq_find_of_eq_true, find_nat_lt, find_mem_find?_decide, find_eq_dite, find_lt_iff, find_of_not_zero, val_find, find?_decide_get_eq_find, find?_decide_eq_dite, find_le
|
init 📖 | CompOp | 31 mathmath: init_def, init_update_last, Finset.map_snocEquiv_filter_piFinset, Finset.card_snocEquiv_filter_piFinset, SchwartzMap.iteratedPDeriv_succ_right, take_init, iteratedFDerivWithin_succ_apply_right, continuousMultilinearCurryRightEquiv_symm_apply, Filter.Tendsto.finInit, ContinuousMultilinearMap.norm_map_init_le, ContinuousAt.finInit, linearIndependent_fin_succ', snocOrderIso_symm_apply, take_eq_init, ContinuousMultilinearMap.uncurryRight_apply, partialProd_init, snoc_init_self, iteratedFDeriv_succ_apply_right, tail_init_eq_init_tail, MultilinearMap.uncurryRight_apply, Finset.filter_piFinset_eq_map_snocEquiv, continuousMultilinearCurryRightEquiv_symm_apply', init_update_castSucc, mem_piFinset_iff_last_init, Continuous.finInit, partialSum_init, removeNth_last, init_snoc, LineDeriv.iteratedLineDerivOp_succ_right, comp_init, snocEquiv_symm_apply
|
insertNth 📖 | CompOp | 74 mathmath: insertNth_succ_cons, preimage_insertNth_Icc_of_mem, insertNth_comp_succAbove, MultilinearMap.map_insertNth_add, nndist_insertNth_insertNth, insertNth_rev, ContinuousAlternatingMap.map_insertNth, insertNth_one_right, ContinuousAt.finInsertNth, insertNthEquiv_apply, insertNth_comp_rev, MultilinearMap.map_insertNth_smul, insertNth_le_iff, BoxIntegral.hasIntegral_GP_pderiv, insertNth_mem_piFinset_insertNth, BoxIntegral.hasIntegral_GP_divergence_of_forall_hasDerivWithinAt, insertNth_right_injective, insertNth_apply_succAbove, insertNth_self_removeNth, insertNth_binop, insertNth_injective2, insertNth_mul, MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable_of_equiv, insertNth_apply_below, cons_apply_cycleRange, BoxIntegral.Box.continuousOn_face_Icc, update_insertNth, MultilinearMap.curryMid_apply_apply, MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable', preimage_insertNth_Icc_of_notMem, Continuous.finInsertNth, insertNth_apply_same, succAbove_cases_eq_insertNth, BoxIntegral.Box.mapsTo_insertNth_face, insertNth_zero', Filter.Tendsto.finInsertNth, BoxIntegral.Box.mapsTo_insertNth_face_Icc, RelSeries.insertNth_toFun, insertNth_last', insertNth_apply_above, insertNth_div, insertNth_update, BoxIntegral.norm_volume_sub_integral_face_upper_sub_lower_smul_le, insertNth_last, insertNth_div_same, insertNth_zero, insertNth_mem_Icc, ContinuousMultilinearMap.curryMid_apply, insertNthOrderIso_apply, insertNth_comp_cycleRange_symm, insertNth_add, MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable, insertNth_removeNth, insertNth_zero_right, dist_insertNth_insertNth, prod_insertNth, ContinuousMultilinearMap.norm_map_insertNth_le, AlternatingMap.neg_one_pow_smul_map_insertNth, AlternatingMap.map_insertNth, ContinuousAlternatingMap.neg_one_pow_smul_map_insertNth, le_insertNth_iff, insertNth_eq_iff, insertNth_inj, removeNth_insertNth, sum_insertNth, eq_insertNth_iff, ContinuousWithinAt.finInsertNth, insertNth_left_injective, cons_comp_cycleRange, torusIntegral_succAbove, insertNth_sub, ContinuousOn.finInsertNth, insertNth_apply_cycleRange_symm, insertNth_sub_same
|
insertNthEquiv 📖 | CompOp | 9 mathmath: insertNthEquiv_apply, insertNthEquiv_last, insertNthOrderIso_toEquiv, insertNthEquiv_zero, insertNthEquiv_symm_apply, Finset.filter_piFinset_eq_map_insertNthEquiv, Finset.map_insertNthEquiv_filter_piFinset, MeasurableEquiv.piFinSuccAbove_symm_apply, MeasurableEquiv.piFinSuccAbove_apply
|
removeNth 📖 | CompOp | 37 mathmath: removeNth_zero, removeNth_apply, Finset.card_insertNthEquiv_filter_piFinset, mem_piFinset_iff_pivot_removeNth, removeNth_removeNth_eq_swap, insertNthOrderIso_symm_apply, AlternatingMap.alternatizeUncurryFin_apply, insertNth_self_removeNth, extDeriv_apply_vectorField, ContinuousAlternatingMap.alternatizeUncurryFin_alternatizeUncurryFinCLM_comp_apply, extDerivWithin_apply_vectorField_of_pairwise_commute, AlternatingMap.neg_one_pow_smul_map_removeNth_add_eq_zero_of_eq, removeNth_update_succAbove, insertNthEquiv_symm_apply, AlternatingMap.alternatizeUncurryFin_alternatizeUncurryFinLM_comp_apply, mul_prod_removeNth, Finset.filter_piFinset_eq_map_insertNthEquiv, LinearMap.uncurryMid_apply, extDerivWithin_apply_vectorField, add_sum_removeNth, removeNth_removeNth_heq_swap, ContinuousLinearMap.uncurryMid_apply, removeNth_update, Finset.map_insertNthEquiv_filter_piFinset, extDeriv_apply_vectorField_of_pairwise_commute, removeNth_last, ContinuousAlternatingMap.neg_one_pow_smul_map_removeNth_add_eq_zero_of_eq, insertNth_removeNth, AlternatingMap.uncurryFin_apply, removeNth_fun_const, extDerivWithin_apply, insertNth_eq_iff, removeNth_insertNth, ContinuousLinearMap.norm_map_removeNth_le, eq_insertNth_iff, ContinuousAlternatingMap.alternatizeUncurryFin_apply, extDeriv_apply
|
repeat 📖 | CompOp | 9 mathmath: repeat_one, repeat_zero, repeat_comp_rev, List.ofFn_fin_repeat, repeat_add, repeat_rev, repeat_succ, repeat_apply, take_repeat
|
snoc 📖 | CompOp | 59 mathmath: comp_snoc, exists_linearIndependent_snoc_of_lt_finrank, ContinuousMultilinearMap.norm_map_snoc_le, snoc_inj, snoc_castSucc, snocCases_snoc, FirstOrder.Language.BoundedFormula.realize_ex, snocEquiv_apply, append_right_cons, sum_snoc, snoc_left_injective, MultilinearMap.curryRight_apply, Embedding.coe_snoc, snoc_comp_natAdd, snoc_comp_castSucc, snoc_injective_iff, ContinuousAt.finSnoc, snoc_apply_zero, FirstOrder.Language.BoundedFormula.realize_all, append_left_snoc, cons_comp_rev, append_right_eq_snoc, snoc_eq_cons_rotate, snoc_update, cons_snoc_eq_snoc_cons, range_snoc, snoc_mem_piFinset_snoc, snocOrderIso_apply, snoc_zero, linearIndependent_fin_snoc, append_snoc, snoc_init_self, ContinuousMultilinearMap.curryRight_apply, prod_snoc, insertNth_last', take_succ_eq_snoc, insertNth_last, Continuous.finSnoc, snoc_eq_append, snoc_right_injective, update_snoc_last, MultilinearMap.snoc_add, ContinuousOn.finSnoc, snoc_comp_castAdd, snoc_injective_of_injective, init_snoc, snoc_rev, continuousMultilinearCurryRightEquiv_apply', exists_linearIndependent_snoc_of_lt_rank, ContinuousWithinAt.finSnoc, continuousMultilinearCurryRightEquiv_apply, MultilinearMap.snoc_smul, snoc_last, snoc_comp_rev, snoc_injective2, Filter.Tendsto.finSnoc, snoc_castAdd, cons_rev, continuousMultilinearCurryFin1_apply
|
snocCases 📖 | CompOp | 1 mathmath: snocCases_snoc
|
snocEquiv 📖 | CompOp | 6 mathmath: snocEquiv_apply, Finset.map_snocEquiv_filter_piFinset, insertNthEquiv_last, Finset.filter_piFinset_eq_map_snocEquiv, snocOrderIso_toEquiv, snocEquiv_symm_apply
|
snocInduction 📖 | CompOp | — |
succAboveCases 📖 | CompOp | 1 mathmath: succAbove_cases_eq_insertNth
|
tail 📖 | CompOp | 38 mathmath: removeNth_zero, comp_tail, Finset.map_consEquiv_filter_piFinset, Matrix.vandermonde_succ, RelSeries.tail_toFun, tail_vecCons, Embedding.coe_tail, LineDeriv.iteratedLineDerivOp_succ_left, Finset.filter_piFinset_eq_map_consEquiv, Function.FromTypes.uncurry_apply_succ, ContinuousLinearMap.uncurryLeft_apply, Finsupp.sum_cons', cons_le, iteratedFDerivWithin_succ_apply_left, Finset.card_consEquiv_filter_piFinset, ContinuousLinearMap.norm_map_tail_le, cons_self_tail, consEquiv_symm_apply, ContinuousAt.finTail, linearIndependent_fin_succ, consOrderIso_symm_apply, tail_init_eq_init_tail, range_fin_succ, partialProd_succ', Continuous.finTail, Filter.Tendsto.finTail, tail_update_succ, SchwartzMap.iteratedPDeriv_succ_left, partialSum_succ', tail_update_zero, le_cons, mem_piFinset_iff_zero_tail, tail_def, continuousMultilinearCurryLeftEquiv_symm_apply, consEquivL_symm_apply, LinearMap.uncurryLeft_apply, tail_cons, iteratedFDeriv_succ_apply_left
|