Created
April 28, 2021 23:09
-
-
Save alexjbest/57d5fead003dddd6931e8c0edcccc364 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| #print ProFiltPseuNormGrp.Top.of.compact_space | |
| #print differential_object.iso_of_components_inv_f | |
| #print add_monoid_hom.id_mem_filtration | |
| #print breen_deligne.universal_map.π_suitable | |
| #print Profinite.iso_of_homeo | |
| #print Mbar.ext_iff | |
| #print polyhedral_lattice.HomZ_map_equiv | |
| #print breen_deligne.data.system_res_def | |
| #print Mbar.Tinv_aux_ne_zero | |
| #print rescale.Tinv' | |
| #print breen_deligne.FreeMat.iso_mk'_hom | |
| #print breen_deligne.data.pow | |
| #print normed_group_hom.norm_mk_lt' | |
| #print NSH_h_res | |
| #print polyhedral_lattice.conerve.int.div_eq_zero | |
| #print pseudo_normed_group.filtration_pi_equiv_symm_apply_coe | |
| #print breen_deligne.basic_universal_map.eval_of | |
| #print LCP | |
| #print breen_deligne.basic_universal_map.eval_LCFP_comp | |
| #print differential_object.lift_functor_nat_iso_hom_app | |
| #print profinitely_filtered_pseudo_normed_group_hom.bound | |
| #print filter.eventually_at_top_prod_self | |
| #print breen_deligne.basic_universal_map.π₁_suitable | |
| #print CLCTinv.map_iso_inv | |
| #print ProFiltPseuNormGrpWithTinv.Top.of.compact_space | |
| #print differential_object.iso_shift'_hom | |
| #print differential_object.complex_like.ext | |
| #print breen_deligne.universal_map.to_functorial_map | |
| #print differential_object.lift_functor_nat_iso | |
| #print NormedGroup.normed_with_aut_Completion | |
| #print CLCPTinv.F_map | |
| #print system_of_complexes.is_weak_bounded_exact.to_exact | |
| #print breen_deligne.data.complex_d_comp_d | |
| #print differential_object.forget_obj | |
| #print punit.profinitely_filtered_pseudo_normed_group_with_Tinv | |
| #print differential_object.lift_functor | |
| #print int.sum_units_to_nat_aux | |
| #print add_monoid_hom.coe_sub | |
| #print system_of_double_complexes.normed_spectral.one_le_K₀ | |
| #print ProFiltPseuNormGrpWithTinv.has_zero | |
| #print LCP.map_norm_noninc | |
| #print breen_deligne.data.system_map_iso_isometry | |
| #print breen_deligne.data.reindex_iso | |
| #print Mbar_le.Tinv_apply | |
| #print system_of_complexes.is_bounded_exact.of_le | |
| #print PolyhedralLattice.Hom_map | |
| #print LCP.T_hom_app_apply_apply | |
| #print succ_equiv_apply | |
| #print breen_deligne.functorial_map.add_comm_group | |
| #print PolyhedralLattice.Cech_conerve.map_succ_zero | |
| #print NormedGroup.norm_incl_eq | |
| #print LCFP.Tinv_app_apply | |
| #print differential_object.iso_shift_one | |
| #print rescale.mem_filtration | |
| #print breen_deligne.data.system_obj_d | |
| #print differential_object.complex_like.iso_app_hom | |
| #print CLCPTinv.map_bound_by | |
| #print nnreal.fact_le_subst_left' | |
| #print differential_object.eq_to_hom_d | |
| #print equiv.curry_symm_apply | |
| #print system_of_complexes.is_weak_bounded_exact.of_iso | |
| #print nnreal.fact_nat_cast_inv_le_one | |
| #print differential_object.neg_f | |
| #print differential_object.complex_like.homotopy.trans_h | |
| #print thm95.universal_constants.N₂_spec' | |
| #print category_theory.arrow.right_func | |
| #print nnreal.fact_inv_mul_le | |
| #print int.extend_from_nat_apply_of_nat | |
| #print differential_object.complex_like.homotopy.comp_const_h | |
| #print CLCFP.res_def' | |
| #print LCFP.T_inv_app | |
| #print breen_deligne.universal_map.σ_suitable | |
| #print profinitely_filtered_pseudo_normed_group.filtration_pi_homeo_symm_apply | |
| #print breen_deligne.functorial_map.has_neg | |
| #print differential_object.iso_shift'_inv | |
| #print polyhedral_lattice_hom.mk_to_add_monoid_hom | |
| #print breen_deligne.FreeMat.mul_functor_map | |
| #print Mbar_le.mk' | |
| #print filter.tendsto.prod_at_top | |
| #print profinitely_filtered_pseudo_normed_group_hom.mk_to_monoid_hom | |
| #print ProFiltPseuNormGrp | |
| #print CLCPTinv.map | |
| #print aux4 | |
| #print NormedGroup.coker.lift_zero | |
| #print FiltrationPow_obj_to_Top_str_is_open | |
| #print profinitely_filtered_pseudo_normed_group_hom.coe_inj | |
| #print LC.T_inv_eq | |
| #print differential_object.complex_like.homotopy.symm_h | |
| #print polyhedral_lattice_hom.to_normed_group_hom_apply | |
| #print equiv.sum_empty_symm_apply_2 | |
| #print nnreal.fact_le_max_left | |
| #print locally_constant.edist_apply_le | |
| #print breen_deligne.data.homotopy_double_h | |
| #print breen_deligne.data.homotopy_double | |
| #print breen_deligne.BD_system_map_app_app | |
| #print nnreal.fact_le_subst_right' | |
| #print finite_free.is_basis | |
| #print differential_object.hom.ext_iff | |
| #print breen_deligne.universal_map.universal_map_equiv_functorial_map_symm_apply | |
| #print CLCP.T_inv | |
| #print add_monoid_hom.mk_polyhedral_lattice_hom' | |
| #print LCFP.Tinv_def | |
| #print Filtration_map_app | |
| #print polyhedral_lattice.iso_of_equiv_of_strict_symm.apply | |
| #print norm_le_zero_iff' | |
| #print breen_deligne.functorial_map.ext | |
| #print ProFiltPseuNormGrpWithTinv.rescale_obj | |
| #print Mbar_le.hom_of_normed_group_hom'_continuous | |
| #print add_monoid_hom.coe_nsmul | |
| #print breen_deligne.functorial_map.has_zero | |
| #print polyhedral_lattice.HomZ_iso | |
| #print function.nsmul_apply | |
| #print profinitely_filtered_pseudo_normed_group_with_Tinv_hom.map_neg | |
| #print CLCFP.res_norm_noninc | |
| #print differential_object.lift_functor_obj | |
| #print profinitely_filtered_pseudo_normed_group.pi_td | |
| #print polyhedral_lattice_hom.strict | |
| #print ProFiltPseuNormGrp.inhabited | |
| #print differential_object.complex_like.to_differential_object_d | |
| #print breen_deligne.universal_map.σ_comp_double | |
| #print breen_deligne.universal_map.from_functorial_map | |
| #print LCP.T_eq | |
| #print differential_object.complex_like.h_comp_d_assoc | |
| #print category_theory.preadditive.comp_gsmul | |
| #print Mbar_le.coe_cast_le | |
| #print LC.T_hom_app_apply_apply | |
| #print polyhedral_lattice_hom.to_add_monoid_hom_injective | |
| #print CLCFP.T_inv_app_apply | |
| #print ProFiltPseuNormGrp.Top.of.t2_space | |
| #print LCFP.res_app_apply | |
| #print breen_deligne.universal_map.eval_double | |
| #print punit.profinitely_filtered_pseudo_normed_group | |
| #print breen_deligne.data.reindex_X | |
| #print CLCTinv.map_iso_hom | |
| #print pseudo_normed_group.filtration_pi_equiv | |
| #print breen_deligne.universal_map.suitable_mul_right_one_le | |
| #print profinitely_filtered_pseudo_normed_group_with_Tinv_hom.inv_of_equiv_of_strict_symm.apply | |
| #print differential_object.complex_like.homotopy.const_comp_h | |
| #print breen_deligne.basic_universal_map.eval_π₂ | |
| #print FiltrationPow.mul_iso_hom | |
| #print differential_object.complex_like.homotopy.comp_h | |
| #print ProFiltPseuNormGrp.coe_of | |
| #print breen_deligne.data.system_obj | |
| #print breen_deligne.universal_map.eval | |
| #print norm_pos_iff' | |
| #print rescale.Tinv'_mem_filtration | |
| #print equiv.curry | |
| #print NormedGroup.parallel_pair_cone | |
| #print differential_object.is_complex_like.iso | |
| #print differential_object.iso_shift_neg_one_inv | |
| #print breen_deligne.basic_universal_map.π₂ | |
| #print differential_object.complex_like.ext' | |
| #print breen_deligne.universal_map.comp_double_double | |
| #print FiltrationPow.mul_iso_inv | |
| #print CLCFP.Tinv_def' | |
| #print system_of_double_complexes.normed_spectral_conditions.h_truncate_zero | |
| #print breen_deligne.data.system_map | |
| #print pseudo_normed_group.filtration_pi_equiv_apply_coe | |
| #print breen_deligne.basic_universal_map.mul_apply | |
| #print normed_group.cauchy_seq_iff | |
| #print add_monoid_hom.const_smul_hom_nat_mem_filtration | |
| #print NormedGroup.LocallyConstant_obj_map | |
| #print ProFiltPseuNormGrpWithTinv.coe_comp_apply | |
| #print FiltrationPow.cast_le_app | |
| #print polyhedral_lattice_hom.map_add | |
| #print CLCFP.T | |
| #print breen_deligne.basic_universal_map.suitable_mul_right | |
| #print breen_deligne.basic_universal_map.pre_eval_π₁ | |
| #print NormedGroup.Completion.lift | |
| #print breen_deligne.data.complex_X | |
| #print breen_deligne.data.fact_two_pow_inv_le_one | |
| #print ProFiltPseuNormGrpWithTinv.Top.of.totally_disconnected_space | |
| #print differential_object.complex_like.d_comp_d_assoc | |
| #print thm95.universal_constants.K₀ | |
| #print differential_object.iso_shift_zero_hom_f | |
| #print Filtration.res_refl | |
| #print breen_deligne.data.σ_f | |
| #print polyhedral_lattice.HomZ_map_inverse_strict | |
| #print controlled_sum_of_mem_closure_range | |
| #print breen_deligne.data.hom_pow | |
| #print differential_object.complex_like.iso_of_components_hom_f | |
| #print normed_group_hom.lift_unique | |
| #print differential_object.iso_shift' | |
| #print succ_pred | |
| #print differential_object.iso_shift_zero | |
| #print system_of_double_complexes.d'_d' | |
| #print differential_object.iso_shift_neg_one_hom | |
| #print cauchy_seq_iff' | |
| #print nnreal.fact_le_subst_right | |
| #print differential_object.mk_complex_like_iso_inv | |
| #print polyhedral_lattice_hom.has_zero | |
| #print breen_deligne.basic_universal_map.suitable_mul_left_one_le | |
| #print FiltrationPow.cast_le_vcomp_Tinv | |
| #print polyhedral_lattice_hom.map_neg | |
| #print breen_deligne.basic_universal_map.eval_π₁ | |
| #print differential_object.shift_obj_d | |
| #print category_theory.arrow.left_to_right | |
| #print CLCP.T | |
| #print differential_object.complex_like.iso_app_inv | |
| #print pseudo_normed_group.mem_filtration_prod | |
| #print breen_deligne.data.complex_d | |
| #print category_theory.functor.map_complex_like'_obj_X | |
| #print category_theory.preadditive.gsmul_comp | |
| #print breen_deligne.universal_map.double_zero | |
| #print breen_deligne.data.hom_pow'_sum' | |
| #print LCP.T | |
| #print ProFiltPseuNormGrpWithTinv.concrete_category | |
| #print LCFP.T_inv_app_apply | |
| #print polyhedral_lattice_hom.coe_mk_polyhedral_lattice_hom' | |
| #print NormedGroup.truncate.map_f_2 | |
| #print profinitely_filtered_pseudo_normed_group_hom.id | |
| #print profinitely_filtered_pseudo_normed_group_with_Tinv_hom.inhabited | |
| #print cauchy_seq_const | |
| #print system_of_double_complexes.truncate_obj_obj_d_f | |
| #print Mbar.nnnorm_sum_le | |
| #print normed_group_hom.equalizer.lift_ι | |
| #print breen_deligne.map_to_pi_add_ext | |
| #print cauchy_seq.subseq_subseq_mem | |
| #print pseudo_normed_group.filtration_prod_equiv_symm_apply_coe | |
| #print filter.tendsto.prod_map_prod_at_top | |
| #print ProFiltPseuNormGrpWithTinv.rescale | |
| #print pseudo_normed_group.neg_mem_filtration_iff | |
| #print finset.eq_sum_range_sub' | |
| #print differential_object.ext | |
| #print differential_object.mk_complex_like_iso_hom | |
| #print succ_int | |
| #print int.norm_coe_units | |
| #print aux1 | |
| #print ProFiltPseuNormGrpWithTinv.coe_of | |
| #print int.cast_add_hom'_one | |
| #print breen_deligne.data.complex₂_obj_d | |
| #print profinitely_filtered_pseudo_normed_group_with_Tinv.pi' | |
| #print pred | |
| #print PolyhedralLattice.Cech_conerve.map_succ_zero_aux | |
| #print int.one_mem_filtration | |
| #print LCFP.res_norm_noninc | |
| #print nnreal.fact_inv_le_one | |
| #print breen_deligne.basic_universal_map.eval_LCFP'_not_suitable | |
| #print punit.normed_group | |
| #print NormedGroup.equalizer.map_congr | |
| #print Pow_mul_inv | |
| #print differential_object.category_theory.has_shift | |
| #print NormedGroup.category_theory.limits.has_equalizers | |
| #print system_of_complexes.is_weak_bounded_exact.iff_of_iso | |
| #print normed_group_hom.quotient.is_normed_group.core | |
| #print add_monoid_hom.pow | |
| #print finite_free.basis_type | |
| #print CLCFP.res_app | |
| #print breen_deligne.universal_map.to_functorial_map_f | |
| #print differential_object.complex_like.shift.additive | |
| #print CLCFPTinv₂_obj | |
| #print alt_face_map_cocomplex.coboundary_coboundary_assoc | |
| #print succ_nat | |
| #print breen_deligne.package.map | |
| #print system_of_double_complexes.truncate_obj_obj_X_d | |
| #print chain_complex.mk'_X | |
| #print free_abelian_group.free_predicate.smul_iff | |
| #print LCFP.res_comp_res | |
| #print breen_deligne.universal_map.from_functorial_map_to_functorial_map | |
| #print profinitely_filtered_pseudo_normed_group_hom.map_sub | |
| #print polyhedral_lattice_hom.to_fun_eq_coe | |
| #print system_of_double_complexes.congr | |
| #print chain_complex.mk' | |
| #print differential_object.complex_like.iso_of_components_inv_f | |
| #print NormedGroup.coker.lift_unique | |
| #print aux0 | |
| #print system_of_double_complexes.col_res | |
| #print Filtration.cast_le_to_fun | |
| #print breen_deligne.basic_universal_map.suitable_mul_right_one_le | |
| #print ProFiltPseuNormGrpWithTinv.Top.of.t2_space | |
| #print breen_deligne.basic_universal_map.double | |
| #print profinitely_filtered_pseudo_normed_group.pi_lift | |
| #print breen_deligne.universal_map.eval_CLCFP_sub | |
| #print ProFiltPseuNormGrpWithTinv.rescale_map_to_fun | |
| #print breen_deligne.basic_universal_map.eval_comp | |
| #print breen_deligne.universal_map.eval_LCFP_sub | |
| #print CLCTinv.map_nat_app | |
| #print Mbar_bdd.mk' | |
| #print breen_deligne.data.hom_pow'_suitable_strict | |
| #print breen_deligne.package.σ_suitable | |
| #print succ_equiv | |
| #print NormedGroup.LCC_obj_map' | |
| #print breen_deligne.universal_map.le_factor | |
| #print polyhedral_lattice.HomZ_map_equiv_symm_apply | |
| #print controlled_sum_of_mem_closure | |
| #print breen_deligne.functorial_map.zero | |
| #print system_of_complexes.apply_hom_eq_hom_apply | |
| #print differential_object.complex_like.d_comp_h_assoc | |
| #print ProFiltPseuNormGrpWithTinv.coe_comp | |
| #print breen_deligne.data.homotopy_pow | |
| #print CLCPTinv.map_comp | |
| #print NormedGroup.category_theory.limits.has_kernels | |
| #print NormedGroup.Completion_T_inv_eq | |
| #print add_monoid_hom.pow_hom | |
| #print nnreal.fact_one_le_pow | |
| #print profinitely_filtered_pseudo_normed_group_with_Tinv_hom.inv_of_equiv_of_strict.apply | |
| #print breen_deligne.basic_universal_map.suitable_mul_left_le_one | |
| #print Filtration.cast_le_comp | |
| #print cochain_complex.mk'_d' | |
| #print breen_deligne.package.π_suitable' | |
| #print Filtration.Tinv₀_comp_res | |
| #print finite_free.rank_dual | |
| #print Mbar_le.cast_le_apply | |
| #print FiltrationPow_obj_to_Top_α | |
| #print norm_le_insert' | |
| #print differential_object.is_cochain_complex | |
| #print Mbar.coe_sum | |
| #print CLCFP.T_inv_app | |
| #print differential_object.complex_like.to_differential_object_X | |
| #print profinitely_filtered_pseudo_normed_group_hom.comp_to_fun | |
| #print profinitely_filtered_pseudo_normed_group_with_Tinv_hom.mk_to_monoid_hom | |
| #print breen_deligne.basic_universal_map.pre_eval_π₂ | |
| #print PolyhedralLattice.augmentation_map_equalizes | |
| #print Mbar_le.coe_mk | |
| #print rescale.add_comm_monoid | |
| #print ProFiltPseuNormGrp.profinitely_filtered_pseudo_normed_group | |
| #print function.gsmul_apply | |
| #print breen_deligne.data.double | |
| #print CLCPTinv.map_nat | |
| #print PolyhedralLattice.rescale_map_apply | |
| #print pseudo_normed_group.archimedean | |
| #print differential_object.iso_shift_one_hom | |
| #print differential_object.iso_shift_zero_inv_f | |
| #print Pow_mul | |
| #print PolyhedralLattice.coe_id | |
| #print equiv.punit_prod_apply_2 | |
| #print LCFP.obj.normed_with_aut | |
| #print LC.T_inv_app_apply_apply | |
| #print CLCPTinv.F_def | |
| #print chain_complex.mk'_d | |
| #print rescale_constants.one | |
| #print differential_object.iso_app | |
| #print locally_constant.norm_apply_le | |
| #print profinitely_filtered_pseudo_normed_group_hom.map_gsmul | |
| #print CLCFP.res_comp_Tinv | |
| #print breen_deligne.data.very_suitable.of_succ | |
| #print Mbar_bdd.coe_mk | |
| #print profinitely_filtered_pseudo_normed_group_hom.comp | |
| #print profinitely_filtered_pseudo_normed_group_with_Tinv_hom.to_profinitely_filtered_pseudo_normed_group_hom | |
| #print breen_deligne.basic_universal_map.pre_eval_double | |
| #print breen_deligne.universal_map.eval_σ | |
| #print rescale.normed_group | |
| #print profinitely_filtered_pseudo_normed_group.pi_compact | |
| #print profinitely_filtered_pseudo_normed_group_hom.inhabited | |
| #print profinitely_filtered_pseudo_normed_group_with_Tinv_hom.inv_of_equiv_of_strict | |
| #print PolyhedralLattice.rescale | |
| #print generates_norm_of_generates_nnnorm | |
| #print CLCP.T_bound_by | |
| #print LCFP.res_comp_T_inv | |
| #print Filtration.res_app_to_fun_coe | |
| #print breen_deligne.basic_universal_map.eval_LCFP_rescale | |
| #print CLCFP.res_refl | |
| #print NormedGroup.LocallyConstant_obj_map_norm_noninc | |
| #print profinitely_filtered_pseudo_normed_group.pi_t2 | |
| #print Mbar.geom | |
| #print PolyhedralLattice.coe_of | |
| #print breen_deligne.universal_map.very_suitable.mul_right | |
| #print Mbar_le.hom_of_normed_group_hom' | |
| #print pseudo_normed_group.add'_eq | |
| #print Mbar.nnnorm_smul | |
| #print Mbar_le.truncate_mk_seq | |
| #print polyhedral_lattice.conerve.norm_π_one_eq | |
| #print NormedGroup.normed_with_aut_LocallyConstant_T | |
| #print give_better_name | |
| #print Mbar_le.coe_hom_of_normed_group_hom'_apply | |
| #print NormedGroup.truncate.obj_X | |
| #print profinitely_filtered_pseudo_normed_group_with_Tinv_hom.comp_to_fun | |
| #print category_theory.functor.map_complex_like_obj_d | |
| #print breen_deligne.data.reindex | |
| #print CLCFPTinv₂_def | |
| #print category_theory.functor.map_complex_like_nat_trans_app_f | |
| #print matrix.reindex_linear_equiv_sum_empty_symm | |
| #print breen_deligne.package.π_suitable | |
| #print PolyhedralLattice.Cech_conerve_obj | |
| #print breen_deligne.data.reindex_iso_inv_f | |
| #print category_theory.functor.map_complex_like_nat_trans'_app_f | |
| #print breen_deligne.data.complex_obj_d | |
| #print breen_deligne.basic_universal_map.π₁ | |
| #print ProFiltPseuNormGrp.of | |
| #print Filtration.pi_iso | |
| #print differential_object.iso_of_components_hom_f | |
| #print Profinite.iso_of_homeo_inv | |
| #print NormedGroup.inhabited | |
| #print NormedGroup.rescale_map_apply | |
| #print PolyhedralLattice.Cech_conerve.preorder_hom_eq_id | |
| #print NormedGroup.truncate_obj | |
| #print system_of_complexes.truncate_map_app_f | |
| #print breen_deligne.basic_universal_map.pre_eval_apply | |
| #print system_of_complexes.apply_inv_eq_inv_apply | |
| #print profinitely_filtered_pseudo_normed_group.pi_map | |
| #print differential_object.complex_like.shift_obj_d | |
| #print category_theory.functor.map_differential_object_obj_d | |
| #print CLCP.T_inv_eq | |
| #print pseudo_normed_group.archimedean.add_monoid_hom | |
| #print breen_deligne.data.hom_pow'_proj' | |
| #print LCFP.T_inv_app_apply_apply | |
| #print filter.tendsto.subseq_mem | |
| #print NormedGroup.equalizer.map_id | |
| #print nnreal.fact_one_le_two | |
| #print category_theory.arrow.left_func | |
| #print system_of_complexes.truncate_obj_obj_X | |
| #print NormedGroup.truncate_map | |
| #print Mbar_bdd.transition_cast_le | |
| #print chain_complex.mk'_d' | |
| #print breen_deligne.universal_map.factor | |
| #print breen_deligne.universal_map.suitable_congr | |
| #print differential_object.complex_like.h_comp_d | |
| #print breen_deligne.universal_map.eval_CLCFPTinv_sub | |
| #print differential_object.complex_like.shift_map_f | |
| #print profinitely_filtered_pseudo_normed_group_with_Tinv_hom.level_coe | |
| #print NormedGroup.incl_apply | |
| #print eventually_constant_sum | |
| #print polyhedral_lattice_hom.coe_mk_polyhedral_lattice_hom | |
| #print system_of_double_complexes.truncate_obj_map_f_f | |
| #print system_of_double_complexes.d_comp_d | |
| #print fact_le_of_add_one_le | |
| #print profinitely_filtered_pseudo_normed_group.filtration_pi_homeo | |
| #print NormedGroup.LCC_obj_map | |
| #print CLCPTinv.F_obj | |
| #print breen_deligne.package.rank | |
| #print breen_deligne.BD_map₂_app_f | |
| #print breen_deligne.universal_map.π | |
| #print differential_object.is_complex_like | |
| #print normed_group_hom.norm_trivial_quotient_mk | |
| #print generates_norm.generates_nnnorm | |
| #print LCP.T_inv_app_apply_apply_2 | |
| #print Pow_Pow_X | |
| #print breen_deligne.universal_map.eval_CLCFPTinv₂_sub | |
| #print polyhedral_lattice.HomZ_map | |
| #print add_monoid_hom.pow_eval | |
| #print category_theory.functor.additive.comp | |
| #print LCP.T_inv_eq | |
| #print profinitely_filtered_pseudo_normed_group_hom.map_zero | |
| #print breen_deligne.universal_map.eval_of | |
| #print equiv.prod_punit_apply_2 | |
| #print rescale.profinitely_filtered_pseudo_normed_group_with_Tinv | |
| #print rescale.Tinv | |
| #print breen_deligne.universal_map.suitable_mul_left_le_one | |
| #print cochain_complex.mk'_X | |
| #print Mbar_le.coe_mk' | |
| #print category_theory.arrow.limit_cone | |
| #print Mbar.of_mask | |
| #print PolyhedralLattice.Hom_obj | |
| #print CLCFP_rescale | |
| #print Mbar.coe_hom | |
| #print CLCPTinv.map_nat_def | |
| #print monoid_hom.coe_one | |
| #print NormedGroup.rescale_obj | |
| #print has_succ_pred.has_succ | |
| #print breen_deligne.universal_map.eval_π | |
| #print Mbar.archimedean | |
| #print NormedGroup.obj.category_theory.limits.preserves_colimits_of_shape | |
| #print CLCFP.res_app' | |
| #print differential_object.id_f | |
| #print Filtration_obj_map_to_fun | |
| #print ProFiltPseuNormGrp.has_coe_to_sort | |
| #print breen_deligne.basic_universal_map.eval_double | |
| #print pseudo_normed_group.filtration_prod_equiv | |
| #print category_theory.iso.apply | |
| #print differential_object.mk_complex_like_iso | |
| #print breen_deligne.functorial_map | |
| #print system_of_complexes.rescale_obj | |
| #print LCFP_rescale | |
| #print Filtration_obj_obj | |
| #print breen_deligne.split | |
| #print normed_group_hom.equalizer.lift_apply_coe | |
| #print CLCFP.res_comp_res | |
| #print CLCTinv.F_def | |
| #print NormedGroup.normed_with_aut_LCC | |
| #print normed_group.mem_closure_iff | |
| #print int.polyhedral_lattice | |
| #print subgroup.saturated | |
| #print breen_deligne.functorial_map.neg | |
| #print pseudo_normed_group.filtration_obj_to_Top_str | |
| #print pseudo_normed_group.sub_mem_filtration | |
| #print Pow_Pow_X_hom_to_fun | |
| #print system_of_complexes.inv_apply_hom_apply | |
| #print breen_deligne.data.reindex_d | |
| #print pi.nat_apply | |
| #print breen_deligne.universal_map.double | |
| #print cauchy_seq.subseq_mem | |
| #print breen_deligne.split_apply | |
| #print PolyhedralLattice.category_theory.limits.has_zero_morphisms | |
| #print polyhedral_lattice.conerve.L_one | |
| #print profinitely_filtered_pseudo_normed_group_with_Tinv_hom.id_to_fun | |
| #print monoid_hom.coe_mul | |
| #print has_succ_pred | |
| #print locally_constant.map_hom_norm_noninc | |
| #print cauchy_seq.add | |
| #print differential_object.complex_like.homotopy.refl_h | |
| #print breen_deligne.data.BD_pow_X | |
| #print polyhedral_lattice.iso_of_equiv_of_strict.apply | |
| #print NormedGroup.lift_unique | |
| #print breen_deligne.package.map_comp_map | |
| #print strict_mono_forall_of_eventually | |
| #print rescale.Tinv_to_fun | |
| #print LCFP.T | |
| #print rescale.profinitely_filtered_pseudo_normed_group | |
| #print differential_object.complex_like.d_comp_h | |
| #print polyhedral_lattice.HomZ_map_equiv_apply | |
| #print CLCFP.res_comp_T_inv | |
| #print strict_mono_forall_of_frequently | |
| #print subgroup.closure_saturated | |
| #print NormedGroup.coker.lift_comp_eq_lift | |
| #print differential_object.iso_shift_neg_one | |
| #print free_abelian_group.equiv_finsupp_symm_apply | |
| #print breen_deligne.universal_map.suitable_sub | |
| #print differential_object.ext_iff | |
| #print profinitely_filtered_pseudo_normed_group.prod_pi_homeo_pi_prod | |
| #print breen_deligne.data.comp_suitable | |
| #print CLCTinv.map_iso | |
| #print equiv.prod_punit_symm_apply | |
| #print nnreal.one_le_add | |
| #print category_theory.functor.map_differential_object_map_f | |
| #print polyhedral_lattice_hom.coe_inj_iff | |
| #print normed_group_hom.equalizer.map_ι | |
| #print breen_deligne.functorial_map.ext_iff | |
| #print FiltrationPow.cast_le_comp | |
| #print NormedGroup.comp_bound_by | |
| #print equiv.curry_apply | |
| #print differential_object.complex_like.complex_like.iso_app | |
| #print system_of_complexes.is_quotient.surjective | |
| #print breen_deligne.universal_map.coeff_mul | |
| #print pow_equiv | |
| #print breen_deligne.basic_universal_map.comp_double_double | |
| #print Pow_obj | |
| #print CLCP | |
| #print normed_group_hom.norm_quotient_mk_le | |
| #print breen_deligne.data.π | |
| #print int.units_univ | |
| #print Profinite.category_theory.concrete_category | |
| #print equiv.sum_empty_apply | |
| #print profinitely_filtered_pseudo_normed_group_with_Tinv_hom.coe_mk | |
| #print differential_object.mk_complex_like_X | |
| #print pseudo_normed_group.filtration_prod_equiv_apply | |
| #print CLCPTinv | |
| #print differential_object.eq_to_hom_f_assoc | |
| #print PolyhedralLattice.concrete_category | |
| #print Pow_mul_hom | |
| #print finite_free.top_fg | |
| #print PolyhedralLattice.Cech_conerve_map | |
| #print normed_group_hom.norm_zero_eq_zero | |
| #print free_abelian_group.support_smul_nat | |
| #print ProFiltPseuNormGrp.bundled_hom | |
| #print breen_deligne.data.homotopy_two_mul_h | |
| #print int.norm_def | |
| #print locally_constant.normed_group | |
| #print profinitely_filtered_pseudo_normed_group_with_Tinv.pi | |
| #print ProFiltPseuNormGrp.coe_comp_apply | |
| #print breen_deligne.universal_map.factor_neg | |
| #print differential_object.complex_like.htpy_idx_rel₁_tt_nat | |
| #print differential_object.complex_like.htpy_idx_rel₂_tt_nat | |
| #print int.extend_from_nat | |
| #print Filtration.Tinv₀_app | |
| #print finite_free.dual | |
| #print filter.eventually_at_top_prod_self' | |
| #print int.nnnorm_coe_units | |
| #print pseudo_normed_group.filtration.has_zero | |
| #print int.has_succ_pred | |
| #print ProFiltPseuNormGrp.coe_comp | |
| #print finite_free.rank_zero | |
| #print int.norm_coe_nat | |
| #print matrix.kronecker_reindex | |
| #print breen_deligne.universal_map.suitable_of_factor_le | |
| #print polyhedral_lattice.add_monoid_hom.coe_incl_apply | |
| #print NormedGroup.Completion_obj | |
| #print system_of_complexes.congr | |
| #print LCFP.map_norm_noninc | |
| #print NormedGroup.lift_comp_incl | |
| #print LC.T_inv_app_apply_apply_2 | |
| #print category_theory.functor.map_complex_like_map_f | |
| #print add_monoid_hom.coe_mk_from_pi | |
| #print CLCFP_def | |
| #print cauchy_seq_of_eventually_eq | |
| #print breen_deligne.functorial_map.has_add | |
| #print system_of_complexes.hom_apply_comp_inv_apply | |
| #print punit.subtype.subsingleton | |
| #print exact_notation | |
| #print NormedGroup.T_hom_incl | |
| #print profinitely_filtered_pseudo_normed_group_with_Tinv_hom.map_sub | |
| #print pow_pow | |
| #print polyhedral_lattice_hom.ext_iff | |
| #print Mbar.Tinv_ne_zero | |
| #print differential_object.forget_map | |
| #print breen_deligne.universal_map.double_of | |
| #print punit.uniform_space | |
| #print generates_norm_iff_generates_nnnorm | |
| #print breen_deligne.basic_universal_map.mul_iso_eval_FP | |
| #print breen_deligne.basic_universal_map.suitable_of_le | |
| #print breen_deligne.universal_map.to_functorial_map_inj | |
| #print system_of_complexes.is_bounded_exact.of_iso | |
| #print breen_deligne.data.hom_double | |
| #print polyhedral_lattice_hom.map_sub | |
| #print NormedGroup.equalizer.map_nat_id | |
| #print profinitely_filtered_pseudo_normed_group.pi | |
| #print category_theory.arrow.mk_inj | |
| #print category_theory.arrow.category_theory.is_iso | |
| #print breen_deligne.universal_map.to_functorial_map_from_functorial_map | |
| #print system_of_complexes.inv_apply_comp_hom_apply | |
| #print breen_deligne.universal_map.universal_map_equiv_functorial_map_apply | |
| #print Mbar.coe_gsmul | |
| #print breen_deligne.universal_map.factor_sub | |
| #print PolyhedralLattice.iso_mk | |
| #print thm95.universal_constants.one_le_K | |
| #print profinitely_filtered_pseudo_normed_group_hom.ext | |
| #print locally_constant.metric_space | |
| #print differential_object.shift_obj_X | |
| #print aux2 | |
| #print normed_group_hom.norm_quotient_mk | |
| #print pseudo_normed_group.filtration.has_neg | |
| #print breen_deligne.data.hom_double_f | |
| #print locally_constant.map_hom_bound_by | |
| #print breen_deligne.universal_map.eval_CLCFPTinv_zero | |
| #print pseudo_normed_group.prod | |
| #print CLCPTinv.F | |
| #print breen_deligne.equiv_of_equiv | |
| #print breen_deligne.universal_map.suitable_neg | |
| #print NSH_δ_res_f | |
| #print rescale.pseudo_normed_group | |
| #print differential_object.eq_to_hom_f | |
| #print ProFiltPseuNormGrp.Top.of.totally_disconnected_space | |
| #print breen_deligne.FreeMat.mul_functor_obj | |
| #print PolyhedralLattice.rescale_obj | |
| #print breen_deligne.universal_map.very_suitable.zero | |
| #print breen_deligne.basic_universal_map.eval_png_zero | |
| #print LCP.T_bound_by | |
| #print tsum_abs_eq_coe_tsum_nnabs | |
| #print differential_object.iso_shift_one_inv | |
| #print breen_deligne.basic_universal_map.eval_FP_rescale | |
| #print breen_deligne.universal_map.factor_add | |
| #print breen_deligne.data.mul_obj_X | |
| #print NormedGroup.LCC | |
| #print category_theory.functor.map_complex_like'_map | |
| #print CLCFP.T_hom_app_apply | |
| #print differential_object.sub_f | |
| #print breen_deligne.universal_map.suitable_smul_iff | |
| #print differential_object.complex_like.shift_obj_X | |
| #print breen_deligne.punit_equiv | |
| #print differential_object.iso_app_hom | |
| #print NormedGroup.T_hom_eq | |
| #print int.extend_from_nat_apply_nat_add_one | |
| #print differential_object.hom.mk'_f | |
| #print breen_deligne.basic_universal_map.π₂_suitable | |
| #print int.sum_units_to_nat | |
| #print Pow_Pow_X_inv_to_fun | |
| #print differential_object.is_chain_complex | |
| #print locally_constant.has_edist | |
| #print Mbar.Tinv_succ | |
| #print Filtration.cast_le_refl | |
| #print NormedGroup.iso_isometry_of_norm_noninc | |
| #print LCFP.res_refl | |
| #print cochain_complex.ext | |
| #print LCFP.Tinv_norm_noninc | |
| #print zero_of_closure | |
| #print polyhedral_lattice_hom.map_sum | |
| #print breen_deligne.universal_map.universal_map_equiv_functorial_map | |
| #print NormedGroup.has_limit_parallel_pair | |
| #print rescale.Tinv'_apply | |
| #print NormedGroup.has_zero | |
| #print breen_deligne.data.proj_suitable | |
| #print system_of_double_complexes.d'_d | |
| #print breen_deligne.universal_map.suitable_mul_right_le_one | |
| #print system_of_double_complexes.col_X | |
| #print CLCTinv.map_nat_def | |
| #print CLCPTinv.map_comp_map | |
| #print Filtration.res | |
| #print differential_object.complex_like.complex_like.iso_app_inv | |
| #print Mbar.mem_filtration_iff | |
| #print differential_object.mk_complex_like_d | |
| #print NormedGroup.coe_id | |
| #print add_monoid_hom.comp_mem_filtration | |
| #print Mbar.coe_nsmul | |
| #print free_abelian_group.free_predicate.smul_nat_iff | |
| #print differential_object.complex_like.is_complex_like | |
| #print system_of_double_complexes.truncate_map_app_f_f | |
| #print breen_deligne.data.double_X | |
| #print LCFP.T_inv_eq | |
| #print breen_deligne.basic_universal_map.eval_FP_app_to_fun | |
| #print nnreal.fact_le_inv_mul_self | |
| #print Mbar.coeff | |
| #print breen_deligne.universal_map.suitable_mul_left_one_le | |
| #print breen_deligne.data.σ | |
| #print CLCPTinv.map_id | |
| #print coe_succ_equiv | |
| #print differential_object.eq_to_hom_d_assoc | |
| #print LCP.T_inv | |
| #print LCFP.res_app | |
| #print polyhedral_lattice_hom.to_normed_group_hom | |
| #print finite_free.basis_type.fintype | |
| #print LCP.obj.normed_with_aut | |
| #print Mbar.Tinv_zero | |
| #print locally_constant.map_hom_comp | |
| #print monoid_hom.coe_div | |
| #print breen_deligne.universal_map.eval_CLCFP_rescale | |
| #print locally_constant.map_hom_id | |
| #print differential_object.complex_like.homotopy.of_eq_h | |
| #print strict_mono_forall_of_eventually' | |
| #print Mbar.of_mask_to_fun | |
| #print profinitely_filtered_pseudo_normed_group_hom.coe_mk | |
| #print Mbar_le.injective_cast_le | |
| #print NormedGroup.truncate.obj_d | |
| #print breen_deligne.R | |
| #print breen_deligne.split_symm_apply | |
| #print breen_deligne.basic_universal_map.π₂_comp_double | |
| #print NormedGroup.Completion_complete_space | |
| #print breen_deligne.universal_map.factor_le_of_suitable | |
| #print CLCFP.T_inv_app_apply_2 | |
| #print breen_deligne.data.sum_f | |
| #print breen_deligne.universal_map.eval_LCFP_neg | |
| #print breen_deligne.data.double_d | |
| #print NormedGroup.equalizer.F_obj | |
| #print system_of_complexes.truncate_obj_map_f | |
| #print Mbar_bdd.transition_transition | |
| #print LCP.T_inv_app_apply_apply | |
| #print aux3 | |
| #print ProFiltPseuNormGrpWithTinv.coe_id | |
| #print pred_succ | |
| #print NormedGroup.truncate.obj_d_add_one | |
| #print breen_deligne.data.complex₂_obj_X | |
| #print differential_object.iso_of_components | |
| #print int.extend_from_nat_apply_nat | |
| #print LCFP.res_comp_Tinv | |
| #print Mbar_le.has_zero | |
| #print NormedGroup.equalizer.map_nat_app | |
| #print Profinite.iso_of_homeo_hom | |
| #print differential_object.complex_like.shift | |
| #print profinitely_filtered_pseudo_normed_group_hom.map_neg | |
| #print profinitely_filtered_pseudo_normed_group_hom.map_add | |
| #print breen_deligne.data.complex₂_map_f | |
| #print normed_group_hom.normed_group_quotient | |
| #print breen_deligne.universal_map.eval_comp | |
| #print norm_eq_zero_iff' | |
| #print differential_object.mk_complex_like | |
| #print breen_deligne.data.reindex_iso_hom_f | |
| #print FiltrationPow.mul_iso | |
| #print NormedGroup.LocallyConstant_obj_obj | |
| #print differential_object.complex_like.shift_d | |
| #print breen_deligne.L | |
| #print tendsto_at_top_diagonal | |
| #print profinitely_filtered_pseudo_normed_group_with_Tinv_hom.map_zero | |
| #print Mbar.geom_to_fun | |
| #print CLCPTinv.map_norm_noninc | |
| #print Mbar_le.continuous_of_normed_group_hom' | |
| #print Mbar_le.eq_iff_truncate_eq | |
| #print breen_deligne.functorial_map.add | |
| #print profinitely_filtered_pseudo_normed_group_hom.coe_mk' | |
| #print matrix.kronecker_assoc | |
| #print profinitely_filtered_pseudo_normed_group_hom.id_to_fun | |
| #print profinitely_filtered_pseudo_normed_group_hom.has_zero | |
| #print Mbar_le.coe_hom_of_normed_group_hom_apply | |
| #print pseudo_normed_group.filtration_obj_to_Top_α | |
| #print system_of_double_complexes.d_d | |
| #print breen_deligne.basic_universal_map.suitable_mul_right_le_one | |
| #print int.extend_from_nat_apply_neg_succ_of_nat | |
| #print differential_object.lift_functor_d | |
| #print breen_deligne.basic_universal_map.pre_eval | |
| #print Mbar_bdd.has_zero | |
| #print NormedGroup.coe_of | |
| #print Mbar.coe_smul | |
| #print Mbar.coeff_apply | |
| #print CLCFP.map_norm_noninc | |
| #print breen_deligne.universal_map.π_comp_double | |
| #print finite_free.basis | |
| #print system_of_complexes.d_d | |
| #print nnreal.fact_one_le_add_one | |
| #print CLCFP.T_inv_eq | |
| #print category_theory.functor.map_complex_like_obj_X | |
| #print breen_deligne.universal_map.suitable_of_le | |
| #print CLCP.map_norm_noninc | |
| #print system_of_complexes.is_bounded_exact | |
| #print differential_object.iso_app_inv | |
| #print category_theory.functor.map_complex_like'_obj_d | |
| #print breen_deligne.BD_map_app_f | |
| #print NormedGroup.incl | |
| #print differential_object.complex_like.complex_like.iso_app_hom | |
| #print FiltrationPow.Tinv_app_to_fun_coe | |
| #print pred_int | |
| #print finite_free.rank | |
| #print ProFiltPseuNormGrpWithTinv.of_coe | |
| #print profinitely_filtered_pseudo_normed_group_with_Tinv_hom.map_add | |
| #print ProFiltPseuNormGrp.concrete_category | |
| #print torsion_free | |
| #print polyhedral_lattice_hom.coe_injective | |
| #print finset.eq_sum_range_sub | |
| #print CLCTinv.map_nat_iso | |
| #print system_of_double_complexes.d'_comp_d' | |
| #print add_monoid_hom.coe_gsmul | |
| #print breen_deligne.data.preadditive | |
| #print monoid_hom.coe_inv | |
| #print system_of_double_complexes.truncate_obj_obj_X_X | |
| #print polyhedral_lattice.iso_of_equiv_of_strict | |
| #print system_of_complexes.hom_apply_inv_apply | |
| #print breen_deligne.universal_map.eval_comp_double | |
| #print differential_object.lift_functor_map | |
| #print LCFP_def | |
| #print differential_object.shift | |
| #print breen_deligne.basic_universal_map.π₁_comp_double | |
| #print CLCTinv.F_obj | |
| #print system_of_double_complexes.row_X | |
| #print differential_object.complex_like.ext_iff | |
| #print breen_deligne.data.proj_f | |
| #print ProFiltPseuNormGrp.coe_id | |
| #print breen_deligne.universal_map.eval_CLCFPTinv₂_rescale | |
| #print punit.metric_space | |
| #print ProFiltPseuNormGrp.has_zero | |
| #print breen_deligne.FreeMat.double_add | |
| #print profinitely_filtered_pseudo_normed_group.filtration_pi_homeo_apply | |
| #print system_of_complexes.truncate_obj_d_succ_succ | |
| #print profinitely_filtered_pseudo_normed_group_with_Tinv_hom.has_zero | |
| #print pi.coe_nat | |
| #print breen_deligne.data.π_f | |
| #print LCFP.T_hom_app_apply_apply | |
| #print polyhedral_lattice_hom.map_zero | |
| #print differential_object.lift_functor_nat_iso_inv_app | |
| #print cochain_complex.mk'_d | |
| #print NormedGroup.LocallyConstant_map_app | |
| #print breen_deligne.basic_universal_map.eval | |
| #print NormedGroup.neg_norm_noninc | |
| #print profinitely_filtered_pseudo_normed_group.pi_topology | |
| #print CLCTinv.map_iso_isometry | |
| #print breen_deligne.universal_map.σ | |
| #print category_theory.functor.map_differential_object_obj_X | |
| #print breen_deligne.FreeMat.double_comp_double | |
| #print PolyhedralLattice.to_NormedGroup | |
| #print breen_deligne.universal_map.eval_LCFP_rescale | |
| #print thm95.universal_constants.fact_c'_le_k' | |
| #print breen_deligne.data.suitable.of_basic | |
| #print PolyhedralLattice.augmentation_map_aux_apply | |
| #print cauchy_seq_iff | |
| #print Filtration.res_comp | |
| #print differential_object.shift_map_f | |
| #print chain_complex.ext | |
| #print pseudo_normed_group.mem_filtration_pi | |
| #print add_subgroup.topological_closure.is_closed | |
| #print differential_object.complex_like.iso_app | |
| #print ProFiltPseuNormGrpWithTinv.inhabited | |
| #print ProFiltPseuNormGrp.large_category | |
| #print breen_deligne.lift_smul_eq_lift | |
| #print system_of_complexes.truncate_obj_obj_d | |
| #print nnreal.fact_mul_le_of_le_one_right | |
| #print add_monoid_hom.apply_mem_filtration |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment