full_not_challenge_no_namespace.txt

limit_cone'_cone
limit_cone'_is_limit
ulift_obj
has_colimits_of_size
equiv_top
equiv_top_apply_coe
equiv_top_symm_apply
coe_of'
colimit_comparison
direct_sum_bicone
direct_sum_lift_π_assoc
direct_sum_punit_iso
eq_of_is_zero
exact_zmod_nsmul_cast
Ext_is_zero_of_one_lt
free_iso_free'_hom_app
free_iso_free'_hom_app_apply
free_iso_free'_inv_app_apply
free'_obj
hom_product_comparison
injective_of_mono'
is_bilimit_direct_sum_bicone
is_iso_hom_product_comparison
is_limit_pi_fan
ker_map_apply
kernel_iso_ker_hom_ker_subtype
kernel_iso_ker_hom_ker_subtype_apply
kernel_iso_ker_inv_kernel_ι
kernel_iso_ker_inv_kernel_ι_apply
limit_on_nat_torsion_free
map_tensor_add_left
map_tensor_zero_right
projective
of_iso_hom
of_iso_inv
pi_fan
pi_hom_ext
pi_lift
pi_lift_π
pi_lift_π_assoc
pi_π
projective_of_Z_Module_projective
range_mkq_cokernel_iso_range_quotient_inv
range_mkq_cokernel_iso_range_quotient_inv_apply
tensor_curry_equiv_apply
tensor_functor_flip_additive
tensor_functor_obj_obj
tensor_uncurry_curry
to_direct_sum
zero_helper
nsmul_eq_zero
zmod_resolution
zmod_resolution_is_resolution
zmod_resolution_pi
zmod_resolution_pi_f
mk_symm
mk_symm_apply
quotient_congr
symm_mk_apply
ulift_symm_apply
coe_mk_from_pi
comp_mem_filtration
const_smul_hom_int_mem_filtration
const_smul_hom_nat_mem_filtration
eval_mem_filtration
id_mem_filtration
mk_from_pi
mk_from_pi_apply
mk_from_pi_mem_filtration
mk_polyhedral_lattice_hom'
pow
pow_eval
pow_hom
range_eq_top_iff
injective_subtype
as_normed_space'
add_comm_group
down
down_add
down_neg
down_smul
has_norm
inhabited
module
norm_def
normed_add_comm_group
normed_space'
up
augmentation_zero
add_neg_fun_comp
add_neg_fun_comp_id
aux_ineq_mul
add_group_add_symm_apply
equiv_bdd_integer_nat
equiv_compl_R_bdd
equiv_compl_R_bdd_apply
group_mul
group_mul_apply
group_mul_symm_apply
equiv_Icc_bdd_nonneg
equiv_Icc_bdd_nonneg_apply
equiv_Icc_R
equiv_Icc_R_apply
le_one_ge_one
le_one_ge_one_eval
le_one_ge_one_symm_eval
lt_one_gt_one
lt_one_gt_one_eval
lt_one_gt_one_symm_eval
mul_inv
mul_inv_eval
mul_inv_rev
equiv_nat_diag
neg_gt_zero_eval
nonpos_ge_zero_symm_eval
nonneg_equiv_nat
summable_iff_on_nat
int_tsum_shift
mul_inv_fun
mul_inv_fun_comp
mul_inv_fun_comp_id
mul_inv_fun_comp_id_apply
mul_inv_fun_def
my_summable_shift
le_equiv_nat
prod_nat_summable
prod_nat_summable_aux
R
range_equiv_Icc
sum_Icc_sum_tail
summable_shift
sum_range_sum_Icc
sum_range_sum_Icc'
sum_reverse
T
zero_le
matrix
quatro_cone
quatro_cone_acyclic
quatro_cone_d_12'
quatro_cone_d_23'
quatro_cone_d_34'
quatro_cone_X_1
quatro_cone_X_2
quatro_cone_X_3
quatro_cons
quatro_cons_acyclic
quatro_cons_hom
quatro_cons_hom_quasi_iso
to_string_python
bounded_derived_category
additive
category
category_comp_val
category_hom
category_id_val
complete_distinguished_triangle_morphism
cone
Ext
Ext_additive_fst
Ext_homological_fst
Ext_map_app_apply
Ext_obj_map
Ext_obj_obj
forget
faithful
full
forget_distinguished_of_distinguished
forget_map_mk
forget_obj_of
forget_replace_triangle
forget_replace_triangle_distinguished
forget_replace_triangle_hom_hom₁
forget_replace_triangle_hom_hom₂
forget_replace_triangle_hom_hom₃
forget_replace_triangle_inv_hom₁
forget_replace_triangle_inv_hom₂
forget_replace_triangle_inv_hom₃
forget_triangulated_functor_struct
forget_triangulated_functor_struct_comm_shift
forget_triangulated_functor_struct_to_functor
has_shift_functor
has_shift_functor_forget
has_shift_functor_forget_hom_app
has_shift_functor_forget_inv_app
has_shift_functor_map_val
has_shift_functor_obj_val
has_zero_object
bounded_derived_category_hom
ext
ext_iff
has_shift
is_iso_localization_functor_map_of_is_quasi_iso
isomorphic_distinguished
is_zero_zero
lift
lift_map
lift_obj
lift_unique
localization_functor
localization_functor_map_val
localization_functor_obj
localization_iso
localization_iso_hom_val
localization_iso_inv_val
localize_lift
mk_iso
mk_iso_hom_val
mk_iso_inv_val
of
of_val
preadditive
preadditive_hom_group_add_val
preadditive_hom_group_neg_val
preadditive_hom_group_nsmul_val
preadditive_hom_group_sub_val
preadditive_hom_group_zero_val
preadditive_hom_group_zsmul_val
pretriangulated
pretriangulated_contractible_distinguished
pretriangulated_distinguished_cocone_triangle
pretriangulated_distinguished_triangles
replace_triangle
replace_triangle'
replace_triangle_map
replace_triangle_map_comp
replace_triangle'_map_hom₁
replace_triangle_map_hom₁_val
replace_triangle'_map_hom₂
replace_triangle_map_hom₂_val
replace_triangle'_map_hom₃
replace_triangle_map_hom₃_val
replace_triangle_map_id
replace_triangle_mor₁
replace_triangle_mor₂
replace_triangle_mor₃
replace_triangle_obj₁
replace_triangle_obj₂
replace_triangle_obj₃
replace_triangle'_obj_mor₁
replace_triangle'_obj_mor₂
replace_triangle'_obj_mor₃
replace_triangle'_obj_obj₁
replace_triangle'_obj_obj₂
replace_triangle'_obj_obj₃
replace_triangle_rotate
rotate_distinguished_triangle
shift_functor_forget
shift_functor_forget_hom_app
shift_functor_forget_inv_app
shift_functor_localization_functor
shift_functor_localization_functor_hom_app_val
shift_functor_localization_functor_inv_app_val
shift_functor_map_val
shift_functor_val
is_K_projective
zero
zero_is_K_projective
π_lift_id_π
π_lift_id_π_assoc
bounded_homotopy_category_coe_to_fun
e
Ext0_map
Ext0_obj
Ext_coproduct_iso_naturality
Ext_coproduct_iso_naturality'
Ext_iso_hom_apply
Ext_iso_inv_apply
Ext_map_Ext_iso'_assoc
Ext_map_shift_iso_inv
Ext_map_shift_iso_inv_assoc
forget_shift
hom_ext
hom_shift_left_iso
hom_shift_right_iso
hom_single_iso_naturality'
hom_val
inv_lift
lift_comp
lift_comp_lift_comp_assoc
lift_comp_lift_self_assoc
lift_neg
mk_iso_hom
mk_iso_inv
homological_functor
preserves_coproducts_single
replace_triangle_mor₁
replace_triangle_mor₂
replace_triangle_mor₃
replace_triangle_obj₁
replace_triangle_obj₂
replace_triangle_obj₃
shift_equiv_inverse_additive
shift_equiv_symm_inverse_additive
shift_functor_map_lift
shift_functor_obj_val
shift_iso_aux_apply
shift_iso_aux_symm_apply
shift_iso_Ext_map
shift_iso_Ext_map_assoc
shift_of_eq
single_forget
val_as_bdd_above
eval
eval_comp
eval_FP2_comp
eval_FP2'_not_suitable
eval_FP_app_apply
eval_LCFP_comp
eval_LCFP'_not_suitable
eval_of
eval_png₀_coe
pre_eval
pre_eval_apply
proj_aux_kronecker_proj_aux
suitable_mul_left_le_one
suitable_mul_left_one_le
suitable_mul_right_le_one
suitable_mul_right_one_le
suitable_of_le
BD_map₂_app_f
BD_map_app_f
BD_system_map_app_app
additive_whiskering_left
additive_whiskering_right
complex₂_map_f
complex₂_obj_d
complex₂_obj_X
complex_d
complex_d_comp_d
complex_X
comp_suitable
eval_functor'_comp
eval_functor_comp
eval_functor_map_app_f
eval_functor'_map_f
eval_functor'_obj_d
eval_functor_obj_obj_d
eval_functor_obj_obj_X
eval_functor'_obj_X_map
eval_functor'_obj_X_obj
homotopy_two_mul_hom
hom_pow'_proj'
hom_pow'_suitable_strict
hom_pow'_sum'
mul_obj_d
mul_obj_X
preadditive
proj_f
proj_suitable
of_basic
sum_f
system_obj
system_obj_d
system_res_def
eval_Pow_functor_nat_trans_compatibility
FP2_def
res_app
res_comp_res
res_comp_Tinv
res_refl
Tinv_app
Tinv_def
iso_mk'_hom
iso_mk'_inv
mul_functor_map
mul_functor_obj
to_FreeAbMat
Mat
small_category
comm_semiring
aux_hom_app_f
Biprod_iso_Pow_two_components_inv
Biprod_iso_Pow_two_hom_app
Biprod_iso_Pow_two_inv_app
Biprod_obj
endo_T_map_app_f
endo_T_obj_map_f
endo_T_obj_obj_e
endo_T_obj_obj_X
eval'_bounded_above
eval_functor_obj_X
eval_homotopy
eval'_obj_d
eval'_obj_d_0
eval'_obj_X
eval'_obj_X_0
eval'_obj_X_succ
hH0_endo
hH0_endo₂
main_lemma
main_lemma'
Pow_comp_Pow_components_inv
Pow_comp_Pow_hom_app
Pow_comp_Pow_inv_app
Pow_X_hom
Pow_X_inv
congr_eval_Pow'
congr_eval_Pow'_assoc
eval
eval_CLCFP_sub
eval_CLCFPTinv₂_rescale
eval_CLCFPTinv₂_sub
eval_CLCFPTinv_sub
eval_CLCFPTinv_zero
eval_comp
eval_FP2_add
eval_FP2_neg
eval_FP2_of
eval_FP2_sub
eval_LCFP_neg
eval_LCFP_sub
eval_of
eval_Pow'
eval_Pow_comp_app
eval_Pow_functor_obj
eval_Pow'_hcomp
eval_Pow'_of
eval_Pow_zero
eval_Pow_zero_app
factor_add
factor_le_of_suitable
factor_neg
factor_sub
map_eval_Pow
map_eval_Pow'
suitable_congr
suitable_mul_left_le_one
suitable_mul_left_one_le
suitable_mul_right_le_one
suitable_mul_right_one_le
suitable_neg
suitable_of_le
suitable_smul_iff
suitable_sub
mul_right
colim_exact
exact_neg_right_iff
additive_equivalence_inverse
preadditive_yoneda_whiskering_left
whiskering_right
whiskering_right_counit
whiskering_right_unit
yoneda_whiskering_left
conerve_to_cocomplex_homology_is_zero
contracting_homotopy'
face_π
is_contracting_homotopy_zero
op
op_comp_unop
op_hom
op_left
op_right
op_unop
is_splitting_assoc
unop_comp_op
unop_hom
unop_left
unop_op
unop_right
is_biprod
colimit_homology_functor_iso
apply_functor
apply_functor_f
apply_functor_g
apply_functor_X
apply_functor_Y
apply_functor_Z
comp_τ₁
comp_τ₂
comp_τ₃
comp_τ₁
comp_τ₂
comp_τ₃
ext_iff
id_τ₁
id_τ₂
id_τ₃
inhabited
id_τ₁
inhabited
cocomplex_map
to_cocomplex_X
coboundary_coboundary_assoc
cocomplex
to_cocomplex
Sheaf_equiv_of_cover_preserving_cover_lifting_sheafification_compatibility
left_unitor_def
add_f
cocone_X_e
cocone_X_X
cocone_ι_app_f
cokernel_cofork_π_f
cokernel_desc_f
cokernel_obj_X
cokernel_π_f
cone_X_e
cone_X_X
cone_π_app_f
congr_single_functor_inv
flip_map_app_comm
flip_map_app_comm_assoc
flip_obj_map_comm
flip_obj_map_comm_assoc
forget_obj
free_e
map
free_X
free
free_additive
has_colimits
has_limits
ext_iff
is_colimit_cocone_desc_f
is_colimit_cokernel_cofork_desc_f
is_limit_cone_lift_f
is_limit_kernel_fork_lift_f
kernel_fork_iso
kernel_fork_ι_f
kernel_lift_f
kernel_obj_e
kernel_obj_X
kernel_ι_f
mk_bo_ha_ca'_single
mk_bo_ha_ca_single
mk_bo_ho_ca
mk_bo_ho_ca'
neg_f
nsmul_f
pow_comm_assoc
preadditive_yoneda_flip_additive
preserves_colimits
preserves_limits
quot_out_single_map
single_e
single_unEnd
single_unEnd_e
sub_f
tautological_nat_trans_app
twist_cocone_X
twist_cone_X
zsmul_f
eq_to_iso_inv
iso_equiv_apply
iso_equiv_symm_apply
symm_to_adjunction_counit
symm_to_adjunction_unit
eval_functor_colimit_iso
epi_of_exact_zero_right
exact_inr_fst
mono_desc
mono_lift_comp_assoc
arrow_congr
congr
of_op
of_unop
op
d_from_map
epi_of_epi_of_exact
obj_equiv
finite_product_condition'
finite_product_condition_iff_finite_product_condition'
flip_evaluation_comp_whiskering_right
forget₂_additive
homology_iso
is_iso_cokernel_comparison_of_exact
is_proetale_sheaf_of_empty_of_product_of_equalizer
is_proetale_sheaf_of_types_projective
is_singleton_iff_exists_bijective_to_is_singleton
is_singleton_iff_exists_bijective_to_punit
is_singleton_iff_forall_bijective_to_is_singleton
is_singleton_iff_forall_bijective_to_punit
is_zero_of_comp
map_bounded_homotopy_category_map
map_bounded_homotopy_category_obj
map_commsq
map_composable_morphisms_map_τ₁
map_composable_morphisms_map_τ₂
map_composable_morphisms_map_τ₃
map_composable_morphisms_obj_f
map_composable_morphisms_obj_g
map_composable_morphisms_obj_X
map_composable_morphisms_obj_Y
map_composable_morphisms_obj_Z
map_d_to
map_endomorphisms_map_f
map_endomorphisms_obj_e
map_endomorphisms_obj_X
map_homotopy_category_comp_hom_app
map_homotopy_category_comp_inv_app
map_is_biprod
map_next
map_next_iso_inv
map_prev
map_prev_iso_hom
map_short_complex_map_τ₁
map_short_complex_map_τ₂
map_short_complex_map_τ₃
map_short_complex_obj_obj_f
map_short_complex_obj_obj_g
map_short_complex_obj_obj_X
map_short_complex_obj_obj_Y
map_short_complex_obj_obj_Z
obj_biprod_iso
obj_X_next
obj_X_next_hom_eq
obj_X_prev
obj_X_prev_hom_eq
pbool
fintype
preserves_coequalizers_of_exact
preserves_finite_colimits_of_exact
single
map_equiv
whiskering_right_obj_comp
eq_zero_of_forall
is_iso_sheafify_lift_of_is_iso
kernel_fork_point_obj
kernel_fork_X_obj_str_add_coe
kernel_fork_X_obj_str_neg_coe
kernel_fork_X_obj_str_nsmul_coe
kernel_fork_X_obj_str_sub_coe
kernel_fork_X_obj_str_zero_coe
kernel_fork_X_obj_str_zsmul_coe
kernel_fork_X_obj_α
kernel_fork_π_app
has_snake_lemma
homology_functor_preserves_filtered_colimits
homology_iso_inv_homology_functor_map
is_biprod
iso_biprod
iso_biprod_hom
iso_biprod_inv
is_iso_of_is_iso_preadditive_yoneda_map_app
is_iso_sheafification_types_adjunction_counit_app
aux_simp
cokernel_to'
cokernel_to'_mono
eq_δ_of_spec
hom_eq_zero₁
hom_eq_zero₂
map_eq_id
mk_of_short_exact_sequence_hom
row_exact
to_kernel'
to_kernel_epi
δ_spec
cofork_of_cokernel
cofork_of_cokernel_is_colimit
cofork_of_cokernel_is_colimit_desc
cofork_of_cokernel_X
cofork_of_cokernel_ι_app
map_desc_assoc
equalizer_equiv_apply
equalizer_ext
epi_of_epi_of_comp_epi_of_mono
ι_assoc
ι_assoc
fork_of_kernel_is_limit_lift
fork_of_kernel_X
fork_of_kernel_π_app
is_limit_op_fan
is_zero_iff_exact_zero_zero
is_zero_unop
limit_flip_comp_lim_iso_limit_comp_lim'_hom_π_π_assoc
limit_flip_comp_lim_iso_limit_comp_lim'_inv_π_π_assoc
op_fan
preserves_zero_of_preserves_initial
zero_of_epi_comp_zero
map_associator_hom
unflip
cokernel_cofork_X_map
cokernel_cofork_X_obj
cokernel_cofork_ι_app
cokernel_functor_obj
cokernel_kernel_ι_iso_hom
cokernel_kernel_ι_iso_inv
cokernel_obj_iso_π_hom_assoc
conj_by
is_colimit_cokernel_cofork_desc_app
is_limit_kernel_fork_lift_app
kernel_cokernel_π_iso_hom
kernel_cokernel_π_iso_inv
kernel_fork_X_map
kernel_fork_X_obj
kernel_fork_π_app
kernel_functor_obj
kernel_obj_iso_inv_ι_assoc
map_endomorphisms_app_f
map_next
map_prev
unflip
unflip_app_app
unflip_comp
unflip_id
apply_Pow_hom_app
apply_Pow_inv_app
apply_Pow_naturality
eval_Pow_functor_comp
preserves_colimits
Pow_obj
preserves_colimits_of_shape_const_zero
preserves_colimits_of_shape_const_zero_aux
presheaf_to_SheafOfTypes
presheaf_to_SheafOfTypes_iso
presheaf_to_SheafOfTypes_map_val
presheaf_to_SheafOfTypes_obj_val
prod_induction
strong_epi
epi_homology_map_of_pseudoelement
epi
mono
π_iso_cokernel_lift_hom
π_iso_cokernel_lift_hom_assoc
π'_ι
π_ι
π'_ι_assoc
π_ι_assoc
mono_homology_functor_of_pseudoelement
id_apply
pullback_comp_mono_iso
pullback_comp_mono_iso_fst
pullback_comp_mono_iso_fst_assoc
epi_hom_to_kernel
Ext_iso_zero
Ext_single_iso
Ext_single_iso_kernel
homology_zero_iso
hom_to_kernel
is_iso_hom_to_kernel
is_zero_hom_of_is_zero
mono_hom_to_kernel
epi
π_cokernel_iso_of_eq
π_cokernel_iso_of_eq_assoc
right_split
short_exact
cokernel_iso_cokernel_sheaf_hom_π
cokernel_iso_cokernel_sheaf_inv_π
comp_val_assoc
sheafification_adjunction_types
sheafification_adjunction_types_counit_app
sheafification_adjunction_types_hom_equiv_apply
sheafification_adjunction_types_hom_equiv_symm_apply
sheafification_adjunction_types_unit_app
sheafification_types_reflective
mk_hom_val
mk_inv_val
kernel_iso_kernel_sheaf_hom_ι_assoc
kernel_iso_kernel_sheaf_hom_ι_val_assoc
kernel_iso_kernel_sheaf_inv_ι_assoc
kernel_iso_kernel_sheaf_inv_ι_val
kernel_iso_kernel_sheaf_inv_ι_val_assoc
parallel_pair_iso
sheafification_exact
short_exact_sequence
aux_tac
category
has_zero_morphisms
preadditive
comp
comp_fst
comp_fst_assoc
comp_snd
comp_snd_assoc
comp_trd
comp_trd_assoc
exact_inl_snd
exact_of_split
ext
ext_iff
f_comp_g
f_comp_g_assoc
f_nat
f_nat_app
Fst
Fst_additive
Fst_map
Fst_obj
functor
Functor
functor_map
Functor_map_app
functor_map_naturality
Functor_obj
g_nat
g_nat_app
has_nsmul
has_zsmul
hom
ext
ext_iff
hom_inj
hom_inj_injective
sq1
sq1_assoc
sq2
sq2_assoc
hom_zero_fst
hom_zero_snd
hom_zero_trd
id
id_fst
id_snd
id_trd
is_iso_of_fst_of_trd
iso_of_components
iso_of_components'
iso_of_components'_hom_fst
iso_of_components_hom_fst
iso_of_components'_hom_snd
iso_of_components_hom_snd
iso_of_components'_hom_trd
iso_of_components_hom_trd
iso_of_components'_inv_fst
iso_of_components_inv_fst
iso_of_components'_inv_snd
iso_of_components_inv_snd
iso_of_components'_inv_trd
iso_of_components_inv_trd
left_split
splitting
mk_of_split
mk_of_split'
mk_split
mk_split_split
quiver
has_add
has_neg
has_sub
right_split
splitting
Snd
Snd_additive
snd_is_iso
Snd_map
Snd_obj
split
splitting
split
tfae_split
Trd
Trd_additive
Trd_map
Trd_obj
sigma_functor_preserves_epi
sigma_functor_preserves_mono
left_obj_zero_iso_inv
complex
to_complex_X
boundary_boundary_assoc
complex
to_complex
pullback_sheafification_compatibility_hom_apply_val
to_sheafify_pullback_sheafification_compatibility
col_exact_aux
decidable_eq
exact_kernel_ι_self
hom_tac
map_tac
mk_functor'
mk_functor''
mk_of_short_exact_sequence_hom
o_fst
o_le_o
o_snd
snake_input
category
kernel_sequence
mk_of_short_exact_sequence_hom
proj
proj_map
proj_obj
exact_δ
δ
δ_exact
mk_of_homology
row_exact₁_aux
row_exact₂_aux
snake_input
exact
left_split
map
right_split
short_exact
iso_biprod_zero_inv
epi
mono
section_retraction_assoc
splittings_comm
homological_of_exists
homological_of_inv_rotate
homological_of_nat_iso
is_iso_of_is_iso_inv_rotate
is_iso_of_is_iso_of_is_iso
is_iso_of_is_iso_of_is_iso'
is_iso_of_is_iso_rotate
is_iso_triangle_hom_of_is_iso
linear_yoneda_flip_additive
linear_yoneda_flip_homological
mk_triangle_iso_hom_hom₁
mk_triangle_iso_hom_hom₂
mk_triangle_iso_hom_hom₃
mk_triangle_iso_inv_hom₁
mk_triangle_iso_inv_hom₂
mk_triangle_iso_inv_hom₃
neg₃_equiv_counit_iso
neg₃_equiv_functor
neg₃_equiv_inverse
neg₃_equiv_unit_iso
neg₃_functor_map_hom₁
neg₃_functor_map_hom₂
neg₃_functor_map_hom₃
neg₃_functor_obj
neg₃_rotate_hom_app_hom₁
neg₃_rotate_hom_app_hom₂
neg₃_rotate_hom_app_hom₃
neg₃_rotate_inv_app_hom₁
neg₃_rotate_inv_app_hom₂
neg₃_rotate_inv_app_hom₃
neg₃_unit_iso_hom_app_hom₁
neg₃_unit_iso_hom_app_hom₂
neg₃_unit_iso_hom_app_hom₃
neg₃_unit_iso_inv_app_hom₁
neg₃_unit_iso_inv_app_hom₂
neg₃_unit_iso_inv_app_hom₃
neg_iso_hom
neg_iso_inv
of_components_hom_hom₁
of_components_hom_hom₂
of_components_hom_hom₃
of_components_inv_hom₁
of_components_inv_hom₂
of_components_inv_hom₃
triangle_morphism_is_iso_iff
nonneg_inv_rotate_mor₂
nonneg_inv_rotate_obj₁
nonneg_inv_rotate_obj₂
nonneg_inv_rotate_obj₃
nonneg_rotate_mor₁
nonneg_rotate_mor₂
nonneg_rotate_mor₃
nonneg_rotate_neg₃
nonneg_rotate_obj₁
nonneg_rotate_obj₂
nonneg_rotate_obj₃
obj₁_functor
obj₁_functor_map
obj₁_functor_obj
obj₂_functor
obj₂_functor_map
obj₂_functor_obj
obj₃_functor
obj₃_functor_map
obj₃_functor_obj
shift_comm_eq_eq_to_hom
shift_comm_eq_eq_to_hom_assoc
shift_hom₁
shift_hom₂
shift_hom₃
shift_mor₁
shift_mor₂
shift_mor₃
shift_obj₁
shift_obj₂
shift_obj₃
triangle_shift_functor_map
triangle_shift_functor_obj
triangle_shift_functor_ε_hom_app_hom₁
triangle_shift_functor_ε_hom_app_hom₂
triangle_shift_functor_ε_hom_app_hom₃
triangle_shift_functor_ε_inv_app_hom₁
triangle_shift_functor_ε_inv_app_hom₂
triangle_shift_functor_ε_inv_app_hom₃
triangle_shift_functor_μ_hom_app_hom₁
triangle_shift_functor_μ_hom_app_hom₂
triangle_shift_functor_μ_hom_app_hom₃
triangle_shift_functor_μ_inv_app_hom₁
triangle_shift_functor_μ_inv_app_hom₂
triangle_shift_functor_μ_inv_app_hom₃
triangle_shift_map_hom₁
triangle_shift_map_hom₂
triangle_shift_map_hom₃
triangle_shift_obj_mor₁
triangle_shift_obj_mor₂
triangle_shift_obj_mor₃
triangle_shift_obj_obj₁
triangle_shift_obj_obj₂
triangle_shift_obj_obj₃
whisker_left_comp_assoc
yoneda'_equiv_apply
yoneda'_equiv_symm_apply_app
yoneda'_map
yoneda'_obj
cech_iso_zero_hom
cech_iso_zero_inv
ceil_add_le
chain_complex_embed_cofan_iso
chain_complex_embed_cofan_uniformly_bounded
exact_iff_is_zero_homology
exact_of_is_zero_homology
exact_of_mono
exact_zero_fst_iff_mono
exact_zero_snd_iff_epi
mk_ProjectiveResolution
is_zero_homology_of_exact
chain_complex_nat_has_homology
to_bounded_homotopy_category_map
to_bounded_homotopy_category_obj
to_bounded_homotopy_category_obj_val
chain_complex_to_bounded_homotopy_category_preserves_coproducts
CHFPNG₁_to_CHFPNGₑₗ_obj
CHPNG_coe_to_fun
CLCFP_def
map_norm_noninc
res_app
CLCFP_rescale
res_comp_Tinv
res_refl
T
T_hom_app_apply
CLCFPTinv₂_def
CLCFPTinv₂_obj
T_inv_app_apply
T_inv_app_apply_2
Tinv_def'
T_inv_eq
F_def
F_obj
map_iso_hom
map_iso_inv
map_nat_app
map_nat_def
map_nat_iso
ι_range
as_nat_chain_complex_d
as_nat_chain_complex_X
cons
d
cons_d_01
d_comp_d
cons_d_succ
shape
X
cons_X_0
cons_X_succ
cons
comm
f
cons_f_0
cons_f_succ
desc_comp_left
desc_is_iso
desc_spec
homology_zero_zero'
image_to_kernel_epi_of_epi
image_to_kernel_eq_image_to_kernel_of_eq_fst
image_to_kernel_eq_image_to_kernel_of_eq_snd
image_to_kernel_zero_left'
desc
is_iso_cokernel_pi_image_to_kernel_of_zero_of_zero
kernel_iso_X_of_eq_inv
kernel_subobject_map_epi_of_epi
sq_from_epi_of_epi
X_iso_image'_hom
X_iso_image_hom
X_iso_image_inv
X_iso_kernel
X_iso_kernel_hom
X_iso_kernel_inv
X_iso_kernel_of_eq_hom
cochain_complex_int_has_homology
to_nat_chain_complex_map_f
to_nat_chain_complex_obj
image_comp_is_iso_left_comp_ι
inhabited
congr
bicartesian_iff
ext
ext_iff
iso_hom_π
iso_inv_π
neg_iso_inv
of_iso
w_inv_assoc
ι_eq
ι_fst_assoc
ι_iso_hom
ι_iso_inv
ι_snd_assoc
preserves_limits
coe_comp_apply
coe_id_apply
comp_apply
cone_of_pt_X
cone_of_pt_π_app
continuous_of_is_limit
diagram_of_pt_map
diagram_of_pt_obj
filtration_pi_homeo_apply
filtration_pi_homeo_symm_apply
id
neg
strict
zsmul
coe_mk
coe_mk'
copy_to_fun
id_to_fun
inhabited
map_neg
map_sub
mk_to_monoid_hom
to_schfpsng_hom
to_add_monoid_hom_hom_injective
zero_apply
comp_to_fun
has_zero
id_to_fun
inhabited
apply
apply
level_coe
map_neg
map_sub
mk'_apply
mk_to_monoid_hom
as_lvl
as_lvl_add
comp_apply
neg_def
create_hom_from_level
create_hom_from_level_to_fun
create_iso_from_level
create_iso_from_level_add_aux
create_iso_from_level_add_aux_aux
create_iso_from_level_compat_aux
create_iso_from_level_zero_aux
extend_aux'
P1_functor_map
P1_functor_map_app
P1_functor_obj
P1_functor_obj_map
P1_functor_obj_obj
P2_functor_map
P2_functor_map_app
P2_functor_obj
P2_functor_obj_map
P2_functor_obj_obj
Filtration_obj_obj
id_apply
is_limit_ext
level_cone_compatible
level_cone_compatible_assoc
level_create_iso_from_level
level_jointly_faithful
level_jointly_reflects_limits
fac_aux
lift
lift_continuous
lift_fun
lift_fun_map_add
lift_fun_map_zero
lift_strict
lvl
lvl_spec
mem_filtration_iff_of_is_limit
hom_ext
lift_to_fun
lift_unique
lift_π
lift_π_assoc
π_to_fun
rescale_enlarging_iso_hom_app_to_fun
rescale_enlarging_iso_inv_app_to_fun
rescale_map
rescale_obj_M
rescale_obj_str
rescale_to_Condensed_iso
rescale_to_Condensed_iso_hom_app_val_app_apply
rescale_to_Condensed_iso_inv_app_val_app_apply
to_Condensed_obj
faithful
preserves_limits
colimit_iso_Condensed_obj_aux_apply
colimit_iso_Condensed_obj_aux_symm_apply
level_Condensed_diagram'_map_val_app_down_apply_coe
level_Condensed_diagram_map_val_app_down_apply_coe
level_Condensed_diagram'_obj_val_map_down_apply
level_Condensed_diagram_obj_val_map_down_apply
level_Condensed_diagram'_obj_val_obj
level_Condensed_diagram_obj_val_obj
level_map_apply
level_obj
comap_apply
Presheaf_map
Presheaf_obj
rescale₁
rescale_map
rescale_obj
rescale_preserves_limits_of_shape_discrete_quotient
to_Condensed_map
to_Condensed_obj
CompHausFiltPseuNormGrpWithTinv
concrete_category
has_coe_to_sort
large_category
id_apply
injective_of_is_iso
c_iff
nat_down_int_up_c_iff
nat_up_int_up
symm_next
symm_prev
AB5
Condensed_Ab_CondensedSet_adjunction'_counit_app
Condensed_Ab_CondensedSet_adjunction_counit_app
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_CondensedSet_adjunction'_unit_app
Condensed_Ab_CondensedSet_adjunction_unit_app
Condensed_Ab_to_CondensedSet_obj_val
Condensed_Ab_to_CondensedSet_preserves_limits_of_shape_of_filtered
to_free_free_lift
Condensed_Ab_to_presheaf_obj
enough_projectives
has_coproducts_of_shape
has_finite_biproducts
has_finite_colimits
has_finite_limits
has_products_of_shape
has_colimits
has_limits
is_right_adjoint
cokernel_iso_hom_assoc
coproduct_presentation
coproduct_presentation_eq
coproduct_to_colimit_short_exact_sequence
eval_freeAb_iso
eval_freeAb_iso_component_neg
eval_freeAb_iso_component_zero
eval_freeCond'_iso
eval_freeCond'_iso_aux_neg
eval_freeCond'_iso_aux_zero
eval_freeCond'_iso_component_hom_neg
eval_freeCond'_iso_component_hom_zero
evaluation_additive
evaluation_exact
evaluation_obj
exact_colim_of_exact_of_is_filtered
exactness_in_the_middle_part_one
Condensed_ExtrSheaf_equiv_inverse_val
Condensed_ExtrSheafProd_equiv_functor_obj_val
forget_to_CondensedType
is_right_adjoint
forget_to_CondensedType_map
forget_to_CondensedType_obj
half_internal_hom
half_internal_hom_eval_iso
half_internal_hom_iso
homology_evaluation_iso
homology_functor_evaluation_iso
is_iso_iff_ExtrDisc
of_top_ab_map_val
presentation_point_isomorphism
preserves_finite_limits
Condensed_product_iso_biproduct_spec
Condensed_product_iso_biproduct_spec'_assoc
Condensed_product_iso_biproduct_spec_assoc
Condensed_product_iso_product_spec'
Condensed_product_iso_product_spec'_assoc
Condensed_product_iso_product_spec_assoc
Condensed_prod_val_iso_spec'_assoc
Condensed_prod_val_iso_spec_assoc
Profinite_to_presheaf_Ab
coe_val_obj_sigma_equiv
coe_val_obj_sigma_equiv_symm
preserves_limits
evaluation_map
evaluation_obj
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
sigma_cone
sigma_cone_X
sigma_cone_ι_app
CondensedSet_to_Condensed_Ab_iso_hom_app_val
CondensedSet_to_Condensed_Ab_iso_inv_app_val
CondensedSet_to_Condensed_Ab'_map
CondensedSet_to_Condensed_Ab'_obj_val
CondensedSet_to_Condensed_Ab_obj_val
CondensedSet_to_presheaf_obj
val_obj_sigma_equiv_symm_apply
val_obj_sigma_equiv_symm_apply'
short_exact_iff_ExtrDisc
tensor_curry
tensor_curry_eq
tensor_eval_iso
tensor_iso
tensor_uncurry
tensor_uncurry_eq
unsheafified_free_Cech'
condensify_def
condensify_map_comp
condensify_map_zero
condensify_nonstrict_map_add
condensify_nonstrict_map_neg
comap
comap_LC
comap_LC_linear_map
coproduct_eval_iso
whiskering_comp_hom_app_app
whiskering_comp_inv_app_app
get_kind_string
modifiers
has_to_string
comap_equiv
comap_mem_fibre_iff
equiv_bot
fibre
mem_fibre_iff
mem_fibre_iff'
down_two_up
dual_finset_antimono
embed_coproduct_iso
locally_constant_extend_of_empty
embed_unop
le_zero_iff
mul_inv_eq_iff_eq_mul
sub_pos
summable_of_coe_sum_eq
top_zpow_of_pos
zero_le
get_modifiers
lhs_def
rhs_def
ulift_symm_apply_down
eventually_constant
exact_notation
exists_norm_sub_le_mul
get_pi_app_fn
Ext_compute_with_acyclic_naturality_assoc
Ext_coproduct_iso_naturality_inv
Ext_coproduct_iso_naturality_inv_assoc
Ext_coproduct_iso_naturality_shift_assoc
Ext_coproduct_iso_π_assoc
to_AddCommGroup_iso_apply
preadditive_yoneda_obj_obj_CondensedSet_to_Condensed_Ab_apply
ExtQprime_iso_aux_system_obj_aux'_natural_assoc
binary_product_condition
category_hom
category_id_val
coe_fun_eq
compact_space
empty
elim
elim_val
hom_ext
empty_val
ext_iff
lift_lifts'_assoc
of
of_val
sum
desc
desc_val
hom_ext
inl
inl_desc
inl_val
inr
inr_desc
inr_val
sum_val
t2_space
terminal_condition
topological_space
ExtrDisc_to_Profinite_obj
totally_disconnected_space
half_internal_hom
half_internal_hom_val_obj
category_hom
evaluation
evaluation_additive
half_internal_hom
half_internal_hom_val_map
half_internal_hom_val_obj
ext_iff
hom_has_add
hom_has_add_add_val
hom_has_neg
hom_has_neg_neg_val
hom_has_sub
hom_has_sub_sub_val
hom_has_zero
hom_has_zero_zero_val
map_tensor_val_app
preadditive
tensor_curry
tensor_curry_uncurry
tensor_functor
tensor_functor_additive
tensor_functor_flip_additive
tensor_functor_map_app
tensor_functor_obj_map
tensor_functor_obj_obj
tensor_presheaf_map
tensor_presheaf_obj
tensor_uncurry
tensor_uncurry_curry
tensor_val
tensor_curry
tensor_functor_additive
tensor_functor_map_app
tensor_functor_obj_map
tensor_functor_obj_obj
tensor_uncurry
tensor_val_obj
fact_le_of_add_one_le
file_name
filtered_cocone_X_val
filtered_cocone_ι_app_val
Filtration_cast_eq_hom
Filtration_cast_eq_inv
cast_le_apply
Filtration_obj_map_apply
Filtration_obj_obj
pi_iso
cast_le_app
cast_le_vcomp_Tinv
filtration_pow_iso_aux'₀_spec'
filtration_pow_iso_aux'₀_spec'_assoc
filtration_pow_iso_aux'₀_spec_assoc
filtration_pow_iso_aux'_spec'
filtration_pow_iso_aux_spec'
filtration_pow_iso_aux'_spec'_assoc
filtration_pow_iso_aux'_spec_assoc
filtration_pow_iso_aux_spec'_assoc
filtration_pow_iso_aux_spec_assoc
filtration_pow_iso_spec'
filtration_pow_iso_spec'_assoc
filtration_pow_iso_spec_assoc
FiltrationPow_map
mul_iso_hom
mul_iso_inv
FiltrationPow_obj
Tinv_app
Tinv_app_apply_coe
res
res_app_apply_coe
Filtration_rescale
res_comp
res_refl
Tinv₀_app
Tinv₀_comp_res
floor_le
le_ceil
mem_span_iff
prod_attach'
prod_comap
sum_nat_abs_le
Fintype_invpoly_obj_M
Fintype_invpoly_obj_str
iso_of_equiv_hom
iso_of_equiv_inv
LaurentMeasure
Fintype_LaurentMeasures_obj_M
Fintype_LaurentMeasures_obj_str
Fintype_Lbar_obj_M
Fintype_Lbar_obj_str
normed_free_pfpng
normed_free_pfpng_unit
first_target_stmt
FLC_functor'_map
FLC_functor'_obj
floor_add_floor_le
smul_iff
smul_nat_iff
lift_id_map
discrete_quotient_separates_points
free_pfpng_functor_obj_M
free_pfpng_functor_obj_str
functor_coe_to_fun
map_map'
map_unop
functor_prod_eval_iso_spec_assoc
generates_norm_of_generates_nnnorm
comp_lift
comp_lift_assoc
desc_comp
desc_comp_assoc
desc_π
eq_map_of_π_map_ι
fst_eq_zero
fst_snd_eq_zero
iso_inv
iso_ι
lift_ι
lift_π
lift_π_assoc
map_desc_assoc
map_ι_assoc
snd_eq_zero
ι_desc
ι_desc_assoc
ι_eq_desc
π_comp_desc_assoc
π_eq_lift
π_iso
π_map_ι
fact
hom_equiv_evaluation_apply_eq_app_id
hom_equiv_evaluation_symm_apply_val_app_apply
hom_functor'_map
hom_functor_map
hom_functor'_obj_carrier
hom_functor_obj_M
hom_functor'_obj_str
hom_functor_obj_str
lift_map_assoc
map_desc
map_desc_assoc
map_iso_hom
map_iso_inv
biproduct_bicone
biproduct_bicone_fst
biproduct_bicone_inl
biproduct_bicone_inr
biproduct_bicone_is_coprod
biproduct_bicone_is_prod
biproduct_bicone_snd
biproduct_bicone_X
desc
desc_f
fst_f
inl_f
inr
inr_f
biproduct_is_biprod
lift_f
snd
snd_f
biproduct_X
boundaries_arrow_comp_delta_to_boundaries_assoc
boundaries_arrow_comp_delta_to_cycles_assoc
epi
has_binary_biproducts
has_colimits_of_shape
has_colimits_of_size
has_limits_of_size
cokernel_complex_cofork_X_d
cokernel_complex_cofork_X_X
cokernel_complex_cofork_ι_app
cokernel_complex_d
cokernel_complex_desc_f
cokernel_complex_X
colimit_complex_cocone_X
colimit_complex_cocone_ι_app_f
colimit_complex_d
colimit_complex_X
comp_termwise_split_to_cone_homotopy_hom
desc_of_null_homotopic
cone_from_zero
in_map_assoc
lift_of_null_homotopic
map_id
map_out_assoc
cone_to_termwise_split_comp_homotopy
cone_to_termwise_split_comp_homotopy_hom
cone_to_termwise_split_f
cone_to_zero
triangle_functorial
triangleₕ_map_hom₃
triangleₕ_mor₁
triangleₕ_mor₂
triangleₕ_mor₃
triangleₕ_obj₁_as
triangleₕ_obj₂_as
triangleₕ_obj₃_as_d
triangleₕ_obj₃_as_X
triangle_map
triangle_map_hom₁
triangle_map_hom₂
triangle_map_hom₃
triangle_map_id
triangle_mor₁
triangle_mor₂
triangle_mor₃
triangle_obj₁
triangle_obj₂
triangle_obj₃
cone_X
congr_next_functor
congr_prev_functor
cycles_to_homology_app
desc_of_is_colimit_eval_f
d_of_none
d_to_none
embed_eval_iso_of_some_hom_app
embed_eval_iso_of_some_inv_app
embed_eval_is_zero_of_none
embed_homotopy_hom_eq_zero_of_of_none
embed_homotopy_hom_eq_zero_of_to_none
embed_homotopy_hom_some
embed_iso
embed_nat_obj_down_up_pos
embed_nat_obj_down_up_succ
embed_nat_obj_down_up_succ_f
embed_nat_obj_down_up_zero
embed_nat_obj_down_up_zero_pos
homological_complex_embed_preserves_coproducts
embed_short_complex_π_app_τ₁
embed_short_complex_π_app_τ₂
embed_short_complex_π_app_τ₃
X_some
epi_iff_eval
epi_of_eval
epi_prev
epi_prev'
preserves_colimits_of_size
preserves_limits_of_size
eval_functor
eval_functor_equiv
eval_functor_homology_iso
eval_functor_map_f
obj
eval_functor_obj
obj_d
obj_X
exact_next
exact_prev
epi
functor_eval_homology_iso
functor_eval_homology_nat_iso
functor_eval_homology_nat_iso_hom_app_app
functor_eval_homology_nat_iso_inv_app_app
functor_eval_map_app_f
functor_eval_obj
obj_map_f
obj_obj_d
obj_obj_X
homological_complex_has_homology
subsingleton_to_none
desc'_ι
desc'_ι_assoc
homology_to_mod_boundaries_app
π'_lift
π'_lift_assoc
quotient_obj_shift
shift_as
shift_functor_obj_as
comp_X_eq_to_iso
comp_X_eq_to_iso_assoc
homotopy_connecting_hom_of_splittings
homotopy_connecting_hom_of_splittings_hom
X_eq_to_iso_comp
X_eq_to_iso_comp_assoc
hom_single_iso_symm_apply_f
iso_cone_of_termwise_split_hom_hom₁
iso_cone_of_termwise_split_hom_hom₂
iso_cone_of_termwise_split_hom_hom₃
iso_cone_of_termwise_split_inv_hom₁
iso_cone_of_termwise_split_inv_hom₂
iso_cone_of_termwise_split_inv_hom₃
iso_connecting_hom_shift_cone_inv_f
kernel
kernel_complex_d
kernel_complex_fork_X_d
kernel_complex_fork_X_X
kernel_complex_fork_π_app
kernel_complex_lift_f
kernel_complex_X
kernel_d
π
kernel_X
ι
ι_f
ι_mono
lift_of_is_limit_eval_f
limit_complex_cone_X
limit_complex_cone_π_app_f
limit_complex_d
limit_complex_X
mod_boundaries_functor_obj
modify_d
modify_functor_map_f
modify_functor_obj
modify_X
mono_iff_eval
mono_next
mono_next'
next_functor
next_functor_iso_eval
next_functor_map
next_functor_obj
preserves_finite_colimits
preserves_finite_limits
of_termwise_split_epi_commutes_assoc
of_termwise_split_mono_commutes_assoc
op_functor_additive
op_functor_obj
op_X
prev_functor
prev_functor_iso_eval
prev_functor_map
prev_functor_obj
section_X_eq_to_hom
section_X_eq_to_hom_assoc
shift_equiv_counit_app
shift_equiv_counit_inv_app
shift_equiv_unit_app
shift_equiv_unit_inv_app
shift_functor_additive
shift_functor_eq
shift_functor_map_f
shift_functor_obj_d
shift_functor_obj_X
shift_single_obj_hom_f
shift_single_obj_inv_f
shift_X
single_obj_iso_zero
single_shift_hom_app_f
single_shift_inv_app_f
tautological_endomorphism_f_f
termwise_split_epi_desc
termwise_split_epi_desc_f
termwise_split_epi_desc_split_epi
termwise_split_epi_lift
termwise_split_epi_lift_f
termwise_split_epi_lift_retraction
termwise_split_epi_lift_retraction_assoc
termwise_split_epi_retraction
termwise_split_epi_retraction_f
termwise_split_epi_retraction_lift
termwise_split_epi_retraction_lift_aux
termwise_split_mono_factor_homotopy_equiv_hom
termwise_split_mono_factor_homotopy_equiv_homotopy_hom_inv_id
termwise_split_mono_factor_homotopy_equiv_homotopy_inv_hom_id
termwise_split_mono_factor_homotopy_equiv_inv
termwise_split_mono_section_desc_assoc
triangleₕ_map_splittings_hom
triangleₕ_map_splittings_hom_hom₁
triangleₕ_map_splittings_hom_hom₂
triangleₕ_map_splittings_hom_hom₃
triangleₕ_map_splittings_iso
triangleₕ_map_splittings_iso_hom
triangleₕ_map_splittings_iso_inv
triangleₕ_of_termwise_split_mor₁
triangleₕ_of_termwise_split_mor₂
triangleₕ_of_termwise_split_mor₃
triangleₕ_of_termwise_split_obj₁_as
triangleₕ_of_termwise_split_obj₂_as
triangleₕ_of_termwise_split_obj₃_as
triangle_of_termwise_split_mor₁
triangle_of_termwise_split_obj₁
triangle_of_termwise_split_obj₂
triangle_of_termwise_split_obj₃
unop_functor_additive
unop_functor_obj
unop_X
X_eq_to_iso_shift
desc_zero
has_ι
has_π
apply_exact_functor_cofork_is_colimit
apply_exact_functor_fork_is_limit
apply_exact_functor_to_homology_iso_predatum
coker_iso_iso₃_hom_assoc
fac₁_assoc
fac₂_assoc
fac₃_assoc
tautological_κ
is_iso
η_iso
η_iso_hom_assoc
cokernel_f'_eq_π_iso₂_hom_assoc
f'_iso₁_hom_assoc
map_iso
of_both_zeros_cofork_is_colimit
of_both_zeros_fork_is_limit
of_both_zeros_to_homology_iso_predatum_f'
of_both_zeros_to_homology_iso_predatum_K
of_both_zeros_to_homology_iso_predatum_ι
of_both_zeros_to_homology_iso_predatum_π
of_f_is_zero_cofork_is_colimit
of_f_is_zero_fork_is_limit
of_f_is_zero_to_homology_iso_predatum_f'
of_f_is_zero_to_homology_iso_predatum_K
of_f_is_zero_to_homology_iso_predatum_ι
of_f_is_zero_to_homology_iso_predatum_π
of_g_is_zero_cofork_is_colimit
of_g_is_zero_fork_is_limit
of_g_is_zero_to_homology_iso_predatum_f'
of_g_is_zero_to_homology_iso_predatum_K
of_g_is_zero_to_homology_iso_predatum_ι
of_g_is_zero_to_homology_iso_predatum_π
of_homological_complex
tautological'_cofork_is_colimit
tautological_cofork_is_colimit
tautological'_fork_is_limit
tautological_fork_is_limit
tautological'_iso₁
tautological_iso_hom
tautological'_to_homology_iso_predatum
tautological_to_homology_iso_predatum
mono
apply_functor_f'
apply_functor_K
apply_functor_ι
apply_functor_π
cofork_X
fac_assoc
fork_X
map_iso
map_iso_f'
map_iso_K
map_iso_ι
map_iso_π
tautological'_f'
tautological_f'
tautological'_K
tautological_K
tautological'_ι
tautological_ι
tautological'_π
tautological_π
zero₁_assoc
zero₂_assoc
lift_desc
lift_desc'
lift_desc'_of_eq_zero
fac₁_assoc
map_exact_functor_κ
of_g_are_zeros
tautological'_κ
add_left_hom
add_right_hom
is_acyclic_of_iso
is_quasi_iso_cone_π
lift_triangle_map_hom₁
lift_triangle_map_hom₂
lift_triangle_map_hom₃
lift_triangle_obj
quotient_map_sub
quotient_op_functor
quotient_unop_functor
single_map
single_obj_as_d
single_obj_as_X
triangleₕ_of_termwise_split_mem_distinguished_triangles
unop_functor
congr_hom
sub_left_hom
sub_right_hom
index_up_one_eq_set_up_one_range
neg_one_pow_arrow_iso_left_hom_left
neg_one_pow_arrow_iso_left_hom_right
neg_one_pow_arrow_iso_left_inv_left
neg_one_pow_arrow_iso_right_hom_left
neg_one_pow_arrow_iso_right_hom_right
neg_one_pow_arrow_iso_right_inv_left
neg_one_pow_bit0
neg_one_pow_bit1
neg_one_pow_eq_neg_one_npow
neg_one_pow_eq_pow_abs
neg_one_pow_even
neg_one_pow_ite
neg_one_pow_neg
neg_one_pow_neg_one
neg_one_pow_odd
neg_one_pow_smul_iso_hom
neg_one_pow_smul_iso_inv
neg_one_pow_sub
tsum_eq_nat_tsum_of_bdd_below
coe_nnnorm
eval2_to_fun
has_norm
norm_nonneg
map_bound'
nonneg_of_norm_mul_zpow
norm_add
norm_def
nsmul_apply
sub_apply
summable
Tinv_coeff
Tinv_hom_to_fun
to_laurent_measures_nat_trans_app
to_laurent_measures_of_laurent_measures
zpow_strict_anti
zsmul_apply
is_bounded_above_shift
is_clopen_sUnion
is_closed_sUnion
is_locally_constant_iff_clopen_fibers
is_lub_iff
iso_of_zero_of_bicartesian
iso_on_the_left_neg₀_spec
iso_on_the_left_neg₀_spec'_assoc
iso_on_the_left_neg₀_spec_assoc
iso_on_the_left_neg_spec'_assoc
iso_on_the_left_neg_spec_assoc
iso_on_the_left_zero₀_spec
iso_on_the_left_zero₀_spec'_assoc
iso_on_the_left_zero₀_spec_assoc
iso_on_the_left_zero_spec'_assoc
iso_on_the_left_zero_spec_assoc
iso_on_the_right_neg_spec
iso_on_the_right_neg_spec'
iso_on_the_right_neg_spec'_assoc
iso_on_the_right_neg_spec_assoc
iso_on_the_right_zero_spec
iso_on_the_right_zero_spec'
iso_on_the_right_zero_spec'_assoc
iso_on_the_right_zero_spec_assoc
map_apply
map_comp
map_id
condensed
condensedCH
map_bound'
has_continuous_smul
nonneg_of_norm_mul_zpow
norm_add
profinite
profiniteCH
profiniteCH_map
profiniteCH_obj
profinite_comp_PFPNGT₁_to_CHFPNG₁ₑₗ
profinite_map
profinite_obj
cfpng_hom_add
cfpng_hom_neg
add_comm_group
Φ
Φ_eq_ϕ
Φ_natural
to_Lbar_surjective
zsmul_apply
coeff_bound
has_zero
inhabited
transition_cast_le
transition_transition
coeff_apply
extend_commutes_comp_extend_extends''_assoc
extend_commutes_comp_extend_extends'_assoc
geom_to_fun
inhabited
cast_le_apply
coe_cast_le
coe_hom_of_normed_group_hom_apply
coe_mk
eq_iff_truncate_eq
has_zero
inhabited
injective_cast_le
Tinv_apply
truncate_mk_seq
mk_aux'
mk_aux'_apply_to_fun
mk_aux_apply_to_fun
mk_aux_mem_filtration
nnnorm_nsmul
Tinv_aux_ne_zero
Tinv_ne_zero
LCFP_def
map_norm_noninc
normed_with_aut
res_app_apply
LCFP_rescale
res_comp_res
res_comp_Tinv
res_refl
T
T_hom_app_apply_apply
T_inv_app_apply
Tinv_app_apply
T_inv_app_apply_apply
Tinv_def
T_inv_eq
Tinv_norm_noninc
T_hom_app_apply
T_inv_app_apply
T_inv_app_apply_apply
T_inv_eq
lc_to_c
hom_Lbar_cone_X
le_unbundled
to_add_equiv_apply
to_add_equiv_symm_apply
sections
liquid_tensor_experiment_statement
extract_cons_succ_left
extract_zero_right
list_items_aux
list_type_items
list_value_items
continuous_eval
mem_finset_clopen_unique'
dist_def
edist_apply_le
edist_def
locally_constant_eq
eq_sum
eq_sum_of_fintype
has_edist
linear_eval
map_hom_comp
map_zero
metric_space
nnnorm_apply_le_nnnorm
norm_const
norm_const_zero
normed_add_comm_group
normed_space
norm_eq_iff'
norm_zero
sum_apply
uniform_space
lt_of_lt_of_le_unbundled
main
map_homological_complex_embed
maps_comm
mk_pullback_fst
mnot
coe_of''
projective_of_of_projective
quotient_congr
surjective_congr
my_name_to_string
partition
nat_abs_lt_nat_abs_of_nonneg_of_lt
eq_zero_or_exists_eq_add_of_ne_one
injective_pow
monotone_pow
strict_mono_pow
nat_up_int_down_c_iff
natural_fork
abs_eq
bot_eq_zero
div_lt_iff
div_lt_one_of_lt
half_lt_self
inv_le
inv_le_of_le_mul
le_inv_iff_mul_le
le_of_forall_lt_one_mul_le
lt_div_iff
lt_inv_iff_mul_lt
mul_finset_sup
mul_le_iff_le_inv
mul_lt_of_lt_div
mul_sup
sum_div
two_inv_lt_one
fact_inv_mul_le
fact_le_inv_mul_self
fact_le_subst_left'
fact_le_subst_right
fact_le_subst_right'
fact_nat_cast_inv_le_one
fact_one_le_add_one
fact_two_pow_inv_le_one
inv_mul_le_iff
le_self_rpow
fund_thm'
zero_fst_le
r_sub_sum_small
zero_def
zero_le
zpow_le_iff_log
nonstrict_extend_map_add
nonstrict_extend_map_neg
nonstrict_extend_mono
coe_range
normed_free_pfpng_functor_map
normed_free_pfpng_functor_obj_M
normed_free_pfpng_functor_obj_str
normed_snake_dual
normed_space'
normed_space'
NSH_δ_res_f
of_epi_g
to_homology_iso_predatum_π
one_lt_two_r
oof
eq_none_or_eq_some
enum_iso'_symm_apply_coe
monotone_pow
choose_normed_with_aut_T_hom
has_coe_to_fun_condensed_eval
has_continuous_smul
has_continuous_smul_δ_aux
has_continuous_smul_δ_aux₁
has_continuous_smul_δ_aux₂
has_continuous_smul_δ_aux₃
has_p_norm
lp
pBanach_lp_coe_to_fun
nontrivial
lp_type
complete_space
has_coe_to_fun
has_continuous_smul
has_nnnorm
has_norm
has_norm_norm
module
normed_add_comm_group
pseudo_metric_space
summable
triangle
norm_le_of_forall_sum_le
norm_le_of_tendsto
p_banach
smul_normed_hom_apply
sum_rpow_le_norm
sum_rpow_le_of_tendsto
uniform_continuous_coe
pfpng_ctu_const
pfpng_ctu_id
pfpng_ctu_smul_int
pfpng_ctu_smul_nat
sub
PFPNGT₁_to_CHFPNG₁ₑₗ_map_to_fun
PFPNGT₁_to_CHFPNG₁ₑₗ_obj_M
PFPNGT₁_to_CHFPNG₁ₑₗ_obj_str
pi_induced_induced
coe_incl_apply
augmentation_map_equalizes
has_zero_morphisms
finsupp_fin_one_iso_hom
map_succ_zero
map_succ_zero_aux
Cech_conerve_obj
π_hom
epi
coe_id
coe_of
π_is_quotient
filtration_fintype
coe_injective
coe_inj_iff
coe_mk_polyhedral_lattice_hom
coe_mk_polyhedral_lattice_hom'
Hom_cosimplicial_zero_iso_aux_rfl
ext_iff
Hom_finsupp_equiv_apply
Hom_finsupp_iso_hom_to_fun
Hom_finsupp_iso_inv_to_fun_apply
has_zero
map_sub
Hom_map_to_fun
mk_to_add_monoid_hom
Hom_obj
Hom_rescale_hom_symm_apply
to_add_monoid_hom_injective
to_fun_eq_coe
to_normed_group_hom
to_normed_group_hom_apply
profinitely_filtered_pseudo_normed_group
rescale
rescale_map_apply
rescale_obj
rescale_proj
rescale_proj_bound_by
Tinv_apply
to_SemiNormedGroup
unrescale
π_is_quotient
polyhedral_postcompose'_to_add_monoid_hom_apply
polyhedral_postcompose_to_fun
pos_line
Pow
pow_d_le_z
pow_equiv
pow_filtration_hom_ext
Pow_map
Pow_mul
Pow_mul_hom
Pow_mul_inv
Pow_obj
pow_pow
Pow_Pow_X
Pow_Pow_X_hom_apply
Pow_Pow_X_inv_apply
preadditive_yoneda_obj_obj_CondensedSet_to_Condensed_Ab_natural_assoc
preserves_finite_biproducts_Condensed_evaluation
preserves_limits_aux_1
preserves_limits_of_shape_of_filtered_aux
preserves_limits_of_shape_pempty_of_preserves_terminal
presheaf_to_Condensed_Ab_preserves_colimits
presheaf_to_CondensedSet_map
presheaf_to_CondensedSet_obj_val
print_item_crawl
product_iso_biproduct
product_iso_biproduct_spec
product_iso_biproduct_spec'
product_iso_biproduct_spec'_assoc
product_iso_biproduct_spec_assoc
ProFiltPseuNormGrp
comp_apply
id_apply
is_limit_ext
mem_filtration_iff_of_is_limit
PFPNG₁_to_PFPNGₑₗ
lift_π_assoc
product_pow_iso_spec'_assoc
product_pow_iso_spec_assoc
faithful
bundled_hom
coe_comp
coe_comp_apply
coe_id
coe_of
has_forget₂
concrete_category
has_coe_to_sort
has_zero
inhabited
large_category
of
profinitely_filtered_pseudo_normed_group
to_CompHausFilt
to_CompHausFilt_map
to_CompHausFilt_obj_str
to_CompHausFilt_obj_α
compact_space
t2_space
totally_disconnected_space
coe_comp_apply
coe_sum
gadget_cone_X
gadget_cone_π_app
gadget_diagram_fst_fst_app
gadget_diagram_map
gadget_diagram_obj
is_limit_ext
level_map_app_apply
level_obj_map_apply
level_obj_obj
limit_cone_is_limit
map_lvl_cast_lvl_eq_assoc
map_lvl_comp_assoc
preserves_limits
PFPNGT₁_to_PFPNGTₑₗ
product
fan
hom_ext
is_limit
lift
lift_to_fun
lift_unique
lift_π
lift_π_assoc
π
π_to_fun
rescale
rescale_map
rescale_obj_M
rescale_obj_str
rescale_out
rescale_out_app_to_fun
Tinv_limit_add_monoid_hom_apply
coe_comp
coe_of
has_zero
inhabited
apply
iso_of_equiv_of_strict'_inv_apply
apply
of_coe
Pow_mul_comm_obj_equiv_symm_apply
Pow_mul_inv
Pow_obj
Pow_rescale_aux_apply
Pow_rescale_aux_symm_apply
rescale_obj
compact_space
t2_space
totally_disconnected_space
arrow_cone_iso
arrow_cone_iso_hom_hom_left_apply_coe
arrow_cone_iso_hom_hom_right_apply_coe
arrow_cone_iso_inv_hom
arrow_cone_X
arrow_cone_π_app_left_apply
arrow_cone_π_app_right_apply
arrow_diagram_map_left_apply
arrow_diagram_map_right_apply
arrow_diagram_obj_hom_apply
arrow_diagram_obj_left_to_CompHaus_to_Top_str_is_open
arrow_diagram_obj_left_to_CompHaus_to_Top_α
arrow_diagram_obj_right_to_CompHaus_to_Top_str_is_open
arrow_diagram_obj_right_to_CompHaus_to_Top_α
arrow_limit_cone_cone
arrow_limit_cone_is_limit
bdd_add
bdd_LC_iff_comparison
bdd_neg
bdd_weak_dual
comphaus_filtered_pseudo_normed_group
bdd_weak_dual_filtration_homeo
pseudo_normed_group
bdd_zero
bot_initial_desc
Cech_cone_diagram_obj
Cech_cone_is_limit_lift
Cech_cone_X
Cech_cone_π_app
change_cone_X
compact_space_Radon
compact_space_Radon_LC
compact_space_Radon_LC_of_discrete_quotient
continuous_Radon_equiv_Radon_LC
continuous_Radon_equiv_Radon_LC_symm
continuous_Radon_LC_comparison_component_equiv_symm
continuous_weak_dual_LC_to_fun
dense_range_coe₂
discrete_topology_pmz
empty_is_initial
add_comm_group
hom_ext
lift
lift_ι
lift_ι_assoc
extend_commutes_comp_extend_extends_assoc
extend_commutes_inv_app
extend_map
extend_nat_trans_id
extend_nat_trans_whisker_right
extend_obj
extend_unique
fintype_arrow_diagram_map_left
fintype_arrow_diagram_map_right
fintype_arrow_diagram_obj_hom
fintype_arrow_diagram_obj_left
fintype_arrow_diagram_obj_right
free'_lift_val_eq_sheafification_lift
image_stabilizes
is_limit_arrow_cone
is_limit_arrow_cone_lift_left_apply
is_limit_arrow_cone_lift_right_apply
is_limit_left_arrow_cone_lift_apply
is_limit_prod_cone
is_limit_prod_cone_lift_apply
is_limit_Radon_CompHaus_cone
is_limit_Radon_LC_CompHaus_cone
is_limit_Radon_LC_cone
continuous_Radon_LC
linear_map
Radon_LC
weak_dual
is_limit_Radon_png_cone
is_limit_Radon_png_cone_map_level
is_limit_right_arrow_cone_lift_apply
left_arrow_cone_iso_hom_hom_apply_coe
left_arrow_cone_iso_inv_hom
left_arrow_cone_X
left_arrow_cone_π_app_apply
pi_lift_to_fun
pi_proj_to_fun
Tinv₀_coe
Tinv₀_hom_apply
map_Radon
map_Radon_LC
map_Radon_png
normed_free_pfpng
normed_free_pfpng_level_iso
normed_free_pfpng_π
normed_free_pfpng_π_w
profinite_pow_filtration_iso_component_spec'
profinite_pow_filtration_iso_component_spec'_assoc
profinite_pow_filtration_iso_spec'
profinite_pow_filtration_iso_spec'_assoc
prod_cone
prod_cone_X_to_CompHaus_to_Top_str_is_open
prod_cone_X_to_CompHaus_to_Top_α
prod_cone_π_app
prod_iso
prod_iso_hom
prod_iso_inv
hom_ext
Radon
Radon_closed_embedding
Radon_closed_embedding_range_bdd
Radon_CompHaus_comparison
Radon_CompHaus_cone
Radon_CompHaus_functor
Radon_CompHaus_functor_iso_Radon_LC_CompHaus_functor
Radon_equiv_Radon_LC
Radon_functor
Radon_functor_iso_Radon_LC_functor
Radon_homeomorph_Radon_LC
Radon_iso_limit
Radon_iso_Radon_LC
Radon_iso_real_measures
Radon_LC
Radon_LC_closed_embedding
Radon_LC_comparison
Radon_LC_comparison_component_equiv
Radon_LC_comparison_component_equiv_aux
Radon_LC_comparison_component_homeo
Radon_LC_comparison_component_iso
Radon_LC_comparison_naturality_aux
Radon_LC_CompHaus_comparison
Radon_LC_CompHaus_cone
Radon_LC_CompHaus_diagram
Radon_LC_CompHaus_functor
Radon_LC_cone
Radon_LC_functor
Radon_LC_to_fun
Radon_LC_to_fun_continuous
Radon_LC_to_fun_injective
topological_space
Radon_LC_to_Radon
Radon_LC_to_weak_dual
Radon_png
Radon_png_comparison
Radon_png_comparison_component
Radon_png_cone
Radon_png_functor
Radon_png_functor_level_iso
Radon_png_functor_level_iso_component
Radon_png_iso
Radon_to_fun
Radon_to_fun_continuous
Radon_to_fun_injective
topological_space
Radon_to_Radon_LC
Radon_to_weak_dual
right_arrow_cone_iso_hom_hom_apply_coe
right_arrow_cone_iso_inv_hom
right_arrow_cone_X
right_arrow_cone_π_app_apply
sigma_iso_empty
sigma_sum_iso
sum_iso_coprod
swap_cone_left_X
swap_cone_right_X
t2_space_fun_to_R
t2_space_Radon
t2_space_Radon_LC
t2_space_weak_dual
to_Condensed_equiv_apply
to_Condensed_equiv_symm_apply_val_app
Profinite_to_Condensed_map_val
Profinite_to_Condensed_obj
to_normed_free_pfpng
topological_space_bdd_weak_dual_filtration
weak_dual_C_equiv_LC
weak_dual_C_to_LC
weak_dual_LC_to_C
weak_dual_LC_to_fun
why_do_I_need_this
cast_le'_eq_cast_le
coe_sum'
filtration_obj_to_CompHaus_to_Top_str
filtration_obj_to_CompHaus_to_Top_α
filtration_pi_equiv_apply_coe
filtration_pi_equiv_symm_apply_coe
filtration_prod_equiv
filtration_prod_equiv_apply
filtration_prod_equiv_symm_apply_coe
mem_filtration_prod
neg_mem_filtration_iff
pow_incl
pow_incl_apply
pow_incl_injective
prod
has_limits
comp_apply
id_apply
level_map
level_map'
level_map_app
level_obj_map
level_obj_obj
mem_filtration_iff_of_is_limit
neg_nat_trans
to_Ab_map
to_Ab_obj
profinitely_filtered_pseudo_normed_group
profinitely_filtered_pseudo_normed_group_with_Tinv
QprimeFP_map
QprimeFP_sigma_proj_eq_0
Radon_coe_to_fun
add_rpow_le
sum
functor_map
functor_obj_M
functor_obj_str
homeo_filtration_ϖ_ball_preimage
has_zero
neg_apply
pow_nnnorm_sum_le
Sup_eq'
decidable_rel
reorder
add_comm_monoid
one
map_comphaus_filtered_pseudo_normed_group_hom_to_fun
map_strict_comphaus_filtered_pseudo_normed_group_hom_to_fun
Tinv_to_fun
Completion_T_inv_eq
F_obj
map_id
map_nat_app
map_nat_id
forget₂_Ab_obj
iso_rescale_hom
iso_rescale_inv
LCC_obj_map
LocallyConstant_obj_obj
normed_with_aut_Completion
normed_with_aut_LCC
normed_with_aut_LocallyConstant_T
rescale_map_apply
rescale_obj
T_hom_eq
T_hom_incl
truncate_obj
obj_d
obj_d_add_one
obj_X
set_up_one_antitone
set_up_one_def
set_up_one_span
hom_equiv_apply
hom_equiv_symm_apply_val
has_colimit
cocone_X
cocone_ι_app_τ₁
cocone_ι_app_τ₂
cocone_ι_app_τ₃
functor_category_equivalence
functor_category_equivalence_counit_iso
functor_category_equivalence_functor
functor_unit_iso_comp
functor_category_equivalence_inverse
map_τ₁
map_τ₂
map_τ₃
obj_obj_f_app
obj_obj_g_app
obj_obj_X_map
obj_obj_X_obj
obj_obj_Y_map
obj_obj_Y_obj
obj_obj_Z_map
obj_obj_Z_obj
unit_iso
functor_category_equivalence_unit_iso
obj
functor_homological_complex_map_τ₁
functor_homological_complex_map_τ₂
functor_homological_complex_map_τ₃
functor_homological_complex_obj
functor_homological_complex_π₁_iso_eval
functor_homological_complex_π₁_iso_prev_functor
functor_homological_complex_π₂_iso_eval
functor_homological_complex_π₃_iso_eval
functor_homological_complex_π₃_iso_next_functor
functor_lift_map_τ₁
functor_lift_map_τ₂
functor_lift_map_τ₃
functor_lift_obj_obj_f
functor_lift_obj_obj_g
functor_lift_obj_obj_X
functor_lift_obj_obj_Y
functor_lift_obj_obj_Z
functor_nat_iso_mk
functor_nat_iso_mk_hom
functor_nat_iso_mk_inv
hom_mk_τ₁
hom_mk_τ₂
hom_mk_τ₃
preserves_colimits_of_shape
homology_functor_iso_hom_app
homology_functor_iso_inv_app
homology_functor_obj
iso_mk_hom_τ₁
iso_mk_hom_τ₂
iso_mk_hom_τ₃
iso_mk_inv_τ₁
iso_mk_inv_τ₂
iso_mk_inv_τ₃
mk_id_τ₁
mk_id_τ₂
mk_id_τ₃
mk_obj_f
mk_obj_g
mk_obj_X
mk_obj_Y
mk_obj_Z
nat_trans_hom_mk_app_τ₁
nat_trans_hom_mk_app_τ₂
nat_trans_hom_mk_app_τ₃
nat_trans_hom_mk_comp
nat_trans_hom_mk_comp_assoc
nat_trans_hom_mk_id
zero_preserves_colimits_of_shape
ι_middle_map_τ₁
ι_middle_map_τ₂
ι_middle_map_τ₃
ι_middle_obj_obj_f
ι_middle_obj_obj_g
ι_middle_obj_obj_X
ι_middle_obj_obj_Y
ι_middle_obj_obj_Z
ι_middle_π₁_is_zero
π₁_obj
π₁_preserves_colimit
π₂_obj
π₂_preserves_colimit
π₃_obj
π₃_preserves_colimit
sigma_ι_coproduct_eval_iso
sign_vectors_inhabited
coe_inj
coe_to_add_monoid_hom
comp_to_fun
id_to_fun
inhabited
level_add
level_neg
level_zero
map_sub
map_sum
map_zsmul
mk_to_monoid_hom
to_chfpsng_hom_to_fun
coe_mk
coe_to_add_monoid_hom
comp_apply
id_apply
level_coe
map_neg
mk_to_monoid_hom
comap_eq_iff
prod_nat
biprod_fst
biprod_inl
biprod_inr
biprod_snd
iso_hom
iso_inv
op
op_fst
op_inl
op_inr
op_snd
op_symm
op_unop
symm_fst
symm_inl
symm_inr
symm_snd
symm_symm
unop
unop_fst
unop_inl
unop_inr
unop_op
unop_snd
unop_symm
completion
congr
hom_apply_comp_inv_apply
inv_apply_hom_apply
of_le
surjective
iff_of_iso
rescale_obj
ScaleIndexLeft_apply
ScaleIndexLeft_map_app
ScaleIndexLeft_obj_map
ScaleIndexLeft_obj_obj
ScaleIndexRight_apply
ScaleIndexRight_map_app
ScaleIndexRight_obj_map
ScaleIndexRight_obj_obj
shift_sub_id_is_iso
truncate_map_app_f
truncate_obj_d_succ_succ
truncate_obj_d_zero_one
truncate_obj_map_f
truncate_obj_obj_d
truncate_obj_obj_X
col_map_f
col_obj_X
col_res
col_X
congr
d'_comp_d'
d_comp_d
d'_d
d'_d'
d_d
h_truncate_zero
one_le_K₀
row_map_app_f
row_X
d'_zero_one
d_π
truncate_map_app_f_f
truncate_obj_map_f_f
truncate_obj_obj_d_f
truncate_obj_obj_X_d
truncate_obj_obj_X_X
res_π
extract_facts
asyncI
fact_arith
prove_goal_asyncI
aux_y
bdd_floor
eventually_antitone
eventually_le
eventually_le_one
eventually_pos_floor
eventually_pos_y
exists_limit_y
finite_sum
finite_sum'
has_sum_x
limit_neg_geometric
limit_y
summable_floor
summable_nnnorm
summable_norm
summable_ϑ_section
y
ϑ'
ϑ₀
ϑ_eq_ϑ'
ϑ_section
ϑ_surjective
thm94
thm94_weak
thm94_weak'
thm95
Cech_nerve_level_hom_left
Cech_nerve_level_hom'_right
Cech_nerve_level_hom_right
Cech_nerve_level_inv'_left
Cech_nerve_level_inv'_right
Cech_nerve_level_left_map
Cech_nerve_level_map
Cech_nerve_level_obj
CLCFP'_map_app
CLCFP'_obj_map
col_complex_aux_d
col_complex_aux_X
col_complex_level_map
col_complex_level_obj
col_complex_level_obj_d
col_complex_map
col_complex_obj
col_complex_obj_d
col_complex_obj_iso_X_zero
col_complex_rescaled_map
col_complex_rescaled_obj
double_complex_aux_d
double_complex_aux_rescaled_d
double_complex_aux_rescaled_X
double_complex_aux_X
col'_aux_map
col'_aux_obj
col_iso_hom_app_f
col_iso_inv_app_f
col'_map
col'_obj
col_obj_X_zero
double_complex'_map
double_complex_map
double_complex'_obj
double_complex_obj
FLC_complex_arrow_left
FLC_complex_arrow_right
fstₐ_left
fstₐ_right
snd_apply
ι_apply_coe
FLC_complex_map
FLC_complex_obj
sum_hom₀_apply
sum_homₐ_hom
sum_homₐ_left
sum_homₐ_right
profinite
rescale_functor'
additive
rescale_nat_trans'
scale'
scale'_app
scale_factorial_map
scale_factorial_obj
to_rescale'
fact_κ'_le_k'
K₀
N₂_spec'
one_le_K
Tinv_nat_trans_comp_assoc
indicator
indicator_apply
indicator_continuous
indicator_LC
indicator_LC_apply
indicator_one_inverse_image
singleton
Top_to_Condensed_map_val
Top_to_Condensed_obj
tsum_abs_eq_coe_tsum_nnabs
two_mul_lt_two
two_step_resolution
two_step_resolution_ab
two_step_resolution_ab_d
two_step_resolution_ab_projective
two_step_resolution_ab_X
two_step_resolution_d
two_step_resolution_hom
two_step_resolution_hom_ab
two_step_resolution_projective_pid
two_step_resolution_X
topological_space
up_down_up_eq
up_two_index_down_one
up_two_set_down_one
bdd
bdd_comap
bdd_iff_indexed_parition
bdd_LC
bdd_LC_comap
comap
θ_ϕ_exact
ϕ_apply
ϕ_natural