removable.txt

AddCommGroup.add_subgroup.equiv_top_symm_apply
AddCommGroup.colimit_comparison
AddCommGroup.hom_product_comparison
add_comm_group.limit_on_nat_torsion_free
AddCommGroup.tensor_uncurry_curry
AddCommGroup.zmod_resolution_is_resolution
AddCommGroup.zmod_resolution_pi
add_equiv.mk_symm_apply
add_equiv.ulift_symm_apply
add_monoid_hom.comp_mem_filtration
add_monoid_hom.const_smul_hom_int_mem_filtration
add_monoid_hom.const_smul_hom_nat_mem_filtration
add_monoid_hom.eval_mem_filtration
add_monoid_hom.id_mem_filtration
add_monoid_hom.mk_from_pi_mem_filtration
aux_thm69.equiv.group_mul_apply
aux_thm69.equiv.group_mul_symm_apply
aux_thm69.equiv_Icc_bdd_nonneg_apply
aux_thm69.equiv.le_one_ge_one_eval
aux_thm69.equiv.le_one_ge_one_symm_eval
aux_thm69.equiv.lt_one_gt_one_eval
aux_thm69.equiv.lt_one_gt_one_symm_eval
aux_thm69.equiv.mul_inv_eval
aux_thm69.int.nonneg_equiv_nat
aux_thm69.mul_inv_fun_comp_id_apply
aux_thm69.my_summable_shift
aux_thm69.nat.le_equiv_nat
aux_thm69.sum_Icc_sum_tail
bicartesian.quatro_cone_d_12'
bicartesian.quatro_cone_d_23'
bicartesian.quatro_cone_d_34'
bicartesian.quatro_cone_X_1
bicartesian.quatro_cone_X_2
bicartesian.quatro_cone_X_3
bounded_derived_category.complete_distinguished_triangle_morphism
bounded_derived_category.rotate_distinguished_triangle
bounded_homotopy_category.hom_single_iso_naturality'
breen_deligne.basic_universal_map.eval_FP2'_not_suitable
breen_deligne.basic_universal_map.eval_LCFP'_not_suitable
breen_deligne.basic_universal_map.eval_png₀_coe
breen_deligne.basic_universal_map.proj_aux_kronecker_proj_aux
breen_deligne.BD_map₂_app_f
breen_deligne.data.complex₂_obj_d
breen_deligne.data.complex_d_comp_d
breen_deligne.data.eval_functor_comp
breen_deligne.data.hom_pow'_proj'
breen_deligne.data.hom_pow'_sum'
breen_deligne.data.suitable.of_basic
breen_deligne.FP2_def
breen_deligne.FreeMat.iso_mk'_hom
breen_deligne.FreeMat.to_FreeAbMat
breen_deligne.package.Biprod_iso_Pow_two_components_inv
breen_deligne.package.endo_T_obj_obj_e
breen_deligne.package.eval'_obj_X_0
breen_deligne.package.eval'_obj_X_succ
breen_deligne.package.Pow_comp_Pow_components_inv
breen_deligne.universal_map.eval_CLCFPTinv₂_rescale
breen_deligne.universal_map.eval_CLCFPTinv_sub
breen_deligne.universal_map.eval_FP2_of
breen_deligne.universal_map.eval_FP2_sub
breen_deligne.universal_map.eval_Pow_functor_obj
breen_deligne.universal_map.factor_le_of_suitable
breen_deligne.universal_map.factor_sub
breen_deligne.universal_map.suitable_congr
breen_deligne.universal_map.suitable_smul_iff
category_theory.adjunction.whiskering_right_counit
category_theory.adjunction.whiskering_right_unit
category_theory.arrow.conerve_to_cocomplex_homology_is_zero
category_theory.colimit_homology_functor_iso
category_theory.cover_dense.Sheaf_equiv_of_cover_preserving_cover_lifting_sheafification_compatibility
category_theory.discrete.left_unitor_def
category_theory.endomorphisms.mk_bo_ho_ca
category_theory.endomorphisms.mk_bo_ho_ca'
category_theory.eval_functor_colimit_iso
category_theory.exact_inr_fst
category_theory.exact_seq.of_unop
category_theory.functor.d_from_map
category_theory.functor.finite_product_condition_iff_finite_product_condition'
category_theory.functor.flip_evaluation_comp_whiskering_right
category_theory.functor.is_proetale_sheaf_of_empty_of_product_of_equalizer
category_theory.functor.is_proetale_sheaf_of_types_projective
category_theory.functor.is_singleton_iff_exists_bijective_to_punit
category_theory.functor.is_singleton_iff_forall_bijective_to_is_singleton
category_theory.functor.map_commsq
category_theory.functor.map_next_iso_inv
category_theory.functor.map_prev_iso_hom
category_theory.functor.obj_biprod_iso
category_theory.functor.obj_X_next_hom_eq
category_theory.functor.obj_X_prev_hom_eq
category_theory.functor.preserves_finite_colimits_of_exact
category_theory.functor.whiskering_right_obj_comp
category_theory.grothendieck_topology.eq_zero_of_forall
category_theory.grothendieck_topology.is_iso_sheafify_lift_of_is_iso
category_theory.homology_iso_inv_homology_functor_map
category_theory.is_iso_of_is_iso_preadditive_yoneda_map_app
category_theory.is_snake_input.eq_δ_of_spec
category_theory.is_snake_input.hom_eq_zero₁
category_theory.limits.concrete.equalizer_equiv_apply
category_theory.limits.concrete.equalizer_ext
category_theory.limits.is_limit_op_fan
category_theory.limits.is_zero_iff_exact_zero_zero
category_theory.limits.is_zero_unop
category_theory.limits.zero_of_epi_comp_zero
category_theory.monoidal_functor.map_associator_hom
category_theory.nat_trans.kernel_fork_X_map
category_theory.presheaf_to_SheafOfTypes_iso
category_theory.projective.epi_homology_map_of_pseudoelement
category_theory.projective.homology.π_iso_cokernel_lift_hom
category_theory.projective.mono_homology_functor_of_pseudoelement
category_theory.projective.pullback_comp_mono_iso_fst
category_theory.Sheaf.hom.comp_val_assoc
category_theory.sheafification_adjunction_types_counit_app
category_theory.sheafification_adjunction_types_hom_equiv_apply
category_theory.sheafification_adjunction_types_hom_equiv_symm_apply
category_theory.sheafification_adjunction_types_unit_app
category_theory.Sheaf.iso.mk_hom_val
category_theory.Sheaf.iso.mk_inv_val
category_theory.short_exact_sequence.comp_snd_assoc
category_theory.short_exact_sequence.id_fst
category_theory.short_exact_sequence.id_snd
category_theory.short_exact_sequence.id_trd
category_theory.short_exact_sequence.is_iso_of_fst_of_trd
category_theory.short_exact_sequence.mk_of_split'
category_theory.short_exact_sequence.mk_split_split
category_theory.short_exact_sequence.tfae_split
category_theory.sites.pullback_sheafification_compatibility_hom_apply_val
category_theory.snake_diagram.mk_functor''
category_theory.snake.mk_of_homology
category_theory.splitting.splittings_comm
category_theory.triangulated.triangle_morphism_is_iso_iff
category_theory.triangulated.triangle.nonneg_rotate_neg₃
category_theory.triangulated.triangle.obj₁_functor
category_theory.triangulated.triangle.obj₂_functor
category_theory.triangulated.triangle.obj₃_functor
category_theory.triangulated.triangle.shift_comm_eq_eq_to_hom
category_theory.triangulated.triangle.shift_hom₁
category_theory.triangulated.triangle.shift_hom₂
category_theory.triangulated.triangle.shift_hom₃
category_theory.triangulated.triangle.shift_mor₁
category_theory.triangulated.triangle.shift_mor₂
category_theory.triangulated.triangle.shift_mor₃
category_theory.triangulated.triangle.shift_obj₁
category_theory.triangulated.triangle.shift_obj₂
category_theory.triangulated.triangle.shift_obj₃
chain_complex.exact_zero_fst_iff_mono
chain_complex.exact_zero_snd_iff_epi
chain_complex_nat_has_homology
CLCFP_def
CLCFP.Tinv_def'
CLCTinv.map_nat_iso
cochain_complex.cons_d_01
cochain_complex.cons_d_succ
cochain_complex.cons_X_0
cochain_complex.cons_X_succ
cochain_complex.hom.cons_f_0
cochain_complex.hom.cons_f_succ
cochain_complex.imker.cokernel.desc_comp_left
cochain_complex.imker.cokernel.desc_is_iso
cochain_complex.imker.homology_zero_zero'
cochain_complex.imker.image_to_kernel_eq_image_to_kernel_of_eq_fst
cochain_complex.imker.image_to_kernel_eq_image_to_kernel_of_eq_snd
cochain_complex.imker.image_to_kernel_zero_left'
cochain_complex.imker.is_iso_cokernel_pi_image_to_kernel_of_zero_of_zero
cochain_complex.imker.kernel_subobject_map_epi_of_epi
cochain_complex.imker.sq_from_epi_of_epi
cochain_complex.imker.X_iso_image_inv
cochain_complex_int_has_homology
commsq.ι_iso_inv
CompHaus.coe_id_apply
CompHaus.diagram_of_pt_obj
comphaus_filtered_pseudo_normed_group_hom.strict.to_schfpsng_hom
comphaus_filtered_pseudo_normed_group_hom.to_add_monoid_hom_hom_injective
CompHausFiltPseuNormGrp₁.exact_with_constant.extend_aux'
CompHausFiltPseuNormGrp₁.mem_filtration_iff_of_is_limit
CompHausFiltPseuNormGrp₁.rescale_to_Condensed_iso
CompHausFiltPseuNormGrp.rescale₁
complex_shape.symm_next
complex_shape.symm_prev
Condensed_Ab_CondensedSet_adjunction'_hom_equiv_apply
Condensed_Ab_CondensedSet_adjunction_hom_equiv_apply
Condensed_Ab_CondensedSet_adjunction'_hom_equiv_symm_apply
Condensed_Ab_CondensedSet_adjunction_hom_equiv_symm_apply
Condensed_Ab_to_presheaf_obj
Condensed.coproduct_to_colimit_short_exact_sequence
Condensed.eval_freeAb_iso_component_neg
Condensed.eval_freeAb_iso_component_zero
Condensed.evaluation_exact
Condensed.exactness_in_the_middle_part_one
Condensed_ExtrSheaf_equiv_inverse_val
Condensed.half_internal_hom_eval_iso
Condensed.homology_evaluation_iso
Condensed.homology_functor_evaluation_iso
Condensed.is_iso_iff_ExtrDisc
Condensed.of_top_ab_map_val
Condensed_product_iso_product_spec'
CondensedSet.coe_val_obj_sigma_equiv_symm
CondensedSet.is_colimit_sigma_cone
CondensedSet_presheaf_adjunction_counit_app
CondensedSet_presheaf_adjunction_hom_equiv_apply
CondensedSet_presheaf_adjunction_hom_equiv_symm_apply
CondensedSet_presheaf_adjunction_unit_app
Condensed.tensor_uncurry_eq
condensify_def
condensify_map_zero
condensify_nonstrict_map_add
condensify_nonstrict_map_neg
dual_finset_antimono
embedding.locally_constant_extend_of_empty
ennreal.mul_inv_eq_iff_eq_mul
ennreal.summable_of_coe_sum_eq
ennreal.top_zpow_of_pos
eventually_constant
exact_notation
Ext_coproduct_iso_naturality_inv
ExtQprime_iso_aux_system_comm_setup.add_equiv.to_AddCommGroup_iso_apply
ExtQprime_iso_aux_system_comm_setup.preadditive_yoneda_obj_obj_CondensedSet_to_Condensed_Ab_apply
ExtrDisc_to_Profinite_obj
ExtrSheaf.half_internal_hom_val_obj
ExtrSheafProd.half_internal_hom_val_obj
ExtrSheafProd.tensor_functor_map_app
ExtrSheafProd.tensor_functor_obj_map
ExtrSheafProd.tensor_presheaf_map
ExtrSheafProd.tensor_uncurry_curry
ExtrSheaf.tensor_functor_map_app
ExtrSheaf.tensor_functor_obj_map
ExtrSheaf.tensor_val_obj
fact_le_of_add_one_le
FiltrationPow.cast_le_vcomp_Tinv
filtration_pow_iso_aux'₀_spec'
filtration_pow_iso_aux'_spec'
filtration_pow_iso_aux_spec'
filtration_pow_iso_spec'
FiltrationPow_map
FiltrationPow.mul_iso_hom
Filtration_rescale
Filtration.Tinv₀_comp_res
finset.mem_span_iff
finset.prod_attach'
finset.prod_comap
finset.sum_nat_abs_le
free_abelian_group.free_predicate.smul_nat_iff
free_abelian_group.lift_id_map
functor.map_map'
generates_norm_of_generates_nnnorm
has_homology.desc_π
has_homology.eq_map_of_π_map_ι
has_homology.fst_eq_zero
has_homology.map_ι_assoc
has_homology.π_comp_desc_assoc
hom_equiv_evaluation_apply_eq_app_id
homological_complex.biprod.lift_map_assoc
homological_complex.cone.desc_of_null_homotopic
homological_complex.cone.lift_of_null_homotopic
homological_complex.cone_to_termwise_split_comp_homotopy
homological_complex.cone.triangle_functorial
homological_complex.embed.d_to_none
homological_complex.embed_eval_is_zero_of_none
homological_complex.embed_homotopy_hom_eq_zero_of_of_none
homological_complex.embed_homotopy_hom_eq_zero_of_to_none
homological_complex.embed_homotopy_hom_some
homological_complex.embed_nat_obj_down_up_pos
homological_complex.embed_nat_obj_down_up_succ_f
homological_complex.embed_nat_obj_down_up_zero_pos
homological_complex.embed.X_some
homological_complex.epi_iff_eval
homological_complex.eval_functor_homology_iso
homological_complex.functor_eval_homology_nat_iso
homological_complex.homology.desc'_ι
homological_complex.homology.π'_lift
homological_complex.homotopy_category.quotient_obj_shift
homological_complex.homotopy_category.shift_functor_obj_as
homological_complex.homotopy.comp_X_eq_to_iso
homological_complex.homotopy.X_eq_to_iso_comp
homological_complex.hom_single_iso_symm_apply_f
homological_complex.mono_iff_eval
homological_complex.section_X_eq_to_hom
homological_complex.shift_functor_eq
homological_complex.single_obj_iso_zero
homological_complex.termwise_split_epi_lift_retraction
homological_complex.triangleₕ_map_splittings_iso
homological_complex.triangleₕ_of_termwise_split_mor₃
homology.has_ι
homology.has_π
homology_iso_datum.change.fac₂_assoc
homology_iso_datum.change.fac₃_assoc
homology_iso_datum.tautological'_iso₁
homology_iso_datum.tautological_iso_hom
homology_iso_predatum.fork_X
homology_map_datum.of_g_are_zeros
homotopy_category.quotient_map_sub
homotopy_category.quotient_op_functor
homotopy_category.quotient_unop_functor
homotopy_category.single_map
homotopy_category.triangleₕ_of_termwise_split_mem_distinguished_triangles
index_up_one_eq_set_up_one_range
int.neg_one_pow_bit0
int.neg_one_pow_bit1
int.neg_one_pow_eq_neg_one_npow
int.neg_one_pow_eq_pow_abs
int.neg_one_pow_sub
int.tsum_eq_nat_tsum_of_bdd_below
invpoly.Tinv_coeff
invpoly.Tinv_hom_to_fun
is_clopen.is_clopen_sUnion
is_locally_constant_iff_clopen_fibers
iso_of_zero_of_bicartesian
laurent_measures.condensedCH
laurent_measures.profinite_comp_PFPNGT₁_to_CHFPNG₁ₑₗ
laurent_measures_ses.Φ_natural
laurent_measures.to_Lbar_surjective
Lbar_bdd.transition_cast_le
Lbar_bdd.transition_transition
Lbar_le.coe_hom_of_normed_group_hom_apply
Lbar_le.truncate_mk_seq
Lbar.Tinv_aux_ne_zero
Lbar.Tinv_ne_zero
lem98.hom_Lbar_cone_X
linear_equiv.to_add_equiv_symm_apply
list.extract_cons_succ_left
list.extract_zero_right
locally_constant.density.mem_finset_clopen_unique'
locally_constant.edist_apply_le
locally_constant.edist_def
locally_constant.norm_const_zero
locally_constant.norm_eq_iff'
lt_of_lt_of_le_unbundled
mk_pullback_fst
nat_abs_lt_nat_abs_of_nonneg_of_lt
nat.injective_pow
nnrat.le_inv_iff_mul_le
nnrat.le_of_forall_lt_one_mul_le
nnrat.mul_finset_sup
nnrat.mul_lt_of_lt_div
nnreal.nat.binary.fund_thm'
nnreal.nat.digit.r_sub_sum_small
nonstrict_extend_mono
NSH_δ_res_f
of_epi_g.to_homology_iso_predatum_π
one_lt_two_r
option.eq_none_or_eq_some
pfpng_ctu_smul_int
pi_induced_induced
PolyhedralLattice.augmentation_map_equalizes
PolyhedralLattice.Cech_conerve.finsupp_fin_one_iso_hom
polyhedral_lattice_hom.coe_inj_iff
polyhedral_lattice_hom.coe_mk_polyhedral_lattice_hom'
polyhedral_lattice_hom.mk_to_add_monoid_hom
PolyhedralLattice.Hom_obj
PolyhedralLattice.Hom_rescale_hom_symm_apply
polyhedral_lattice_hom.to_add_monoid_hom_injective
polyhedral_lattice_hom.to_normed_group_hom
PolyhedralLattice.to_SemiNormedGroup
pow_d_le_z
pow_equiv
pow_filtration_hom_ext
Pow_mul_hom
Pow_mul_inv
pow_pow
Pow_Pow_X_hom_apply
ProFiltPseuNormGrp₁.mem_filtration_iff_of_is_limit
ProFiltPseuNormGrpWithTinv₁.gadget_cone_π_app
ProFiltPseuNormGrpWithTinv₁.rescale_out
ProFiltPseuNormGrpWithTinv.iso_of_equiv_of_strict'_inv_apply
ProFiltPseuNormGrpWithTinv.of_coe
ProFiltPseuNormGrpWithTinv.Pow_mul_inv
ProFiltPseuNormGrpWithTinv.Pow_rescale_aux_apply
Profinite.extend_nat_trans_id
Profinite.free'_lift_val_eq_sheafification_lift
profinitely_filtered_pseudo_normed_group_with_Tinv.pi_proj_to_fun
Profinite.normed_free_pfpng_π_w
profinite_pow_filtration_iso_component_spec'
profinite_pow_filtration_iso_spec'
Profinite.Radon_iso_real_measures
pseudo_normed_group.cast_le'_eq_cast_le
pseudo_normed_group.coe_sum'
pseudo_normed_group.filtration_prod_equiv
pseudo_normed_group.mem_filtration_prod
pseudo_normed_group.neg_mem_filtration_iff
pseudo_normed_group.pow_incl_apply
pseudo_normed_group.pow_incl_injective
PseuNormGrp₁.level_map'
PseuNormGrp₁.mem_filtration_iff_of_is_limit
PseuNormGrp₁.neg_nat_trans
QprimeFP_map
QprimeFP_sigma_proj_eq_0
real_measures.homeo_filtration_ϖ_ball_preimage
real.Sup_eq'
SemiNormedGroup.iso_rescale_hom
SemiNormedGroup.LocallyConstant_obj_obj
SemiNormedGroup.T_hom_eq
SemiNormedGroup.truncate.obj_d_add_one
set_up_one_def
set_up_one_span
short_complex.functor_homological_complex_π₁_iso_eval
short_complex.functor_homological_complex_π₃_iso_eval
short_complex.mk_id_τ₁
short_complex.mk_id_τ₂
short_complex.mk_id_τ₃
short_complex.ι_middle_π₁_is_zero
short_complex.π₁_preserves_colimit
short_complex.π₂_preserves_colimit
short_complex.π₃_preserves_colimit
strict_comphaus_filtered_pseudo_normed_group_hom.level_neg
sum_str.op_fst
sum_str.symm_inl
sum_str.unop_fst
system_of_complexes.inv_apply_hom_apply
system_of_complexes.shift_sub_id_is_iso
system_of_complexes.truncate_obj_d_succ_succ
system_of_double_complexes.col_obj_X
system_of_double_complexes.col_res
system_of_double_complexes.col_X
system_of_double_complexes.d'_d'
system_of_double_complexes.row_map_app_f
system_of_double_complexes.row_X
theta.eventually_le_one
theta.ϑ_eq_ϑ'
thm95.Cech_nerve_level_hom_right
thm95.Cech_nerve_level_inv'_left
thm95.Cech_nerve_level_map
thm95.col_complex_level_map
thm95.col_complex_level_obj
thm95.col_complex_level_obj_d
thm95.col_complex_obj_d
thm95.col_complex_obj_iso_X_zero
thm95.double_complex.col'_aux_obj
thm95.double_complex.col_iso_hom_app_f
thm95.double_complex.col_obj_X_zero
thm95.FLC_complex_map
thm95.rescale_nat_trans'
tsum_abs_eq_coe_tsum_nnabs
two_mul_lt_two
two_step_resolution_ab_projective
two_step_resolution_projective_pid
up_down_up_eq
up_two_set_down_one
ϕ_apply
ϕ_natural