| Metric | Count |
|---|
DefinitionsaddCommMonoidTopologicalClosure, topologicalClosure, addCommSemigroupTopologicalClosure, topologicalClosure, addLeft, addRight, mulLeft, mulRight, addUnits, units, Monoid, commMonoidTopologicalClosure, topologicalClosure, commSemigroupTopologicalClosure, topologicalClosure, addHomOfMemClosureRangeCoe, addHomOfTendsto, addMonoidHomOfMemClosureRangeCoe, addMonoidHomOfTendsto, monoidHomOfMemClosureRangeCoe, monoidHomOfTendsto, mulHomOfMemClosureRangeCoe, mulHomOfTendsto | 23 |
TheoremsisClosed_range_coe, continuousConstSMul_nat, continuousSMul_nat, isClosed_range_coe, instContinuousAdd, coe_topologicalClosure, continuousAdd, isClosed_topologicalClosure, le_topologicalClosure, mem_nhds_zero, top_closure_add_self_eq, top_closure_add_self_subset, topologicalClosure_minimal, coe_topologicalClosure, continuousAdd, isClosed_topologicalClosure, le_topologicalClosure, top_closure_add_self_subset, topologicalClosure_minimal, instContinuousAdd, addUnits_map, nsmul, pow, units_map, induced, of_nhds_zero, to_continuousVAdd, to_continuousVAdd_op, nsmul, pow, coe_addLeft, coe_addRight, coe_mulLeft, coe_mulRight, induced, of_nhds_one, to_continuousSMul, to_continuousSMul_op, nsmul, pow, nsmul, pow, add_self, mul_self, add_const, const_add, const_mul, mul_const, nsmul, pow, val_addUnits, val_inv_units, val_neg_addUnits, val_units, const_mul, mul_const, const_mul, mul_const, tendsto_cocompact_mul_left, tendsto_cocompact_mul_right, isOpen_singleton_zero, add, mul, nsmul, pow, add, mul, continuousConstSMul, exists_finset_mulSupport, exists_finset_support, isClosed_range_coe, isClosed_range_coe, instContinuousMul, continuousAdd, continuousAdd', continuousMul, continuousMul', continuousAdd, continuousMul, continuousConstSMul, add, mul, nsmul, pow, coe_topologicalClosure, continuousMul, isClosed_topologicalClosure, le_topologicalClosure, mem_nhds_one, top_closure_mul_self_eq, top_closure_mul_self_subset, topologicalClosure_minimal, coe_topologicalClosure, continuousMul, isClosed_topologicalClosure, le_topologicalClosure, top_closure_mul_self_subset, topologicalClosure_minimal, tendsto_mul_zero_of_disjoint_cocompact_left, tendsto_mul_zero_of_disjoint_cocompact_right, continuousAdd, continuousMul, instContinuousMul, continuousConstVAdd, continuousConstVAdd, addHomOfMemClosureRangeCoe_apply, addHomOfTendsto_apply, addMonoidHomOfMemClosureRangeCoe_apply, addMonoidHomOfTendsto_apply, continuousAdd_iInf, continuousAdd_induced, continuousAdd_inf, continuousAdd_of_comm_of_nhds_zero, continuousAdd_of_discreteTopology, continuousAdd_sInf, continuousAt_nsmul, continuousAt_pow, continuousMul_iInf, continuousMul_induced, continuousMul_inf, continuousMul_of_comm_of_nhds_one, continuousMul_of_discreteTopology, continuousMul_sInf, continuousOn_finset_prod, continuousOn_finset_sum, continuousOn_list_prod, continuousOn_list_sum, continuousOn_multiset_prod, continuousOn_multiset_sum, continuousOn_nsmul, continuousOn_pow, continuous_add_left, continuous_add_right, continuous_finprod, continuous_finprod_cond, continuous_finset_prod, continuous_finset_sum, continuous_finsum, continuous_finsum_cond, continuous_list_prod, continuous_list_sum, continuous_mul_left, continuous_mul_right, continuous_multiset_prod, continuous_multiset_sum, continuous_nsmul, continuous_one, continuous_pow, continuous_zero, eventuallyEq_prod, eventuallyEq_sum, exists_mem_nhds_zero_mul_subset, exists_nhds_one_split, exists_nhds_one_split4, exists_nhds_zero_half, exists_nhds_zero_quarter, exists_open_nhds_one_mul_subset, exists_open_nhds_one_split, exists_open_nhds_zero_add_subset, exists_open_nhds_zero_half, finprod_eventually_eq_prod, finsum_eventually_eq_sum, instContinuousAddAdditiveOfContinuousMul, instContinuousAddOrderDual, instContinuousAddULift, instContinuousMulMultiplicativeOfContinuousAdd, instContinuousMulOrderDual, instContinuousMulULift, isClosed_setOf_map_add, isClosed_setOf_map_mul, isClosed_setOf_map_one, isClosed_setOf_map_zero, le_nhds_add, le_nhds_mul, monoidHomOfMemClosureRangeCoe_apply, monoidHomOfTendsto_apply, mulHomOfMemClosureRangeCoe_apply, mulHomOfTendsto_apply, nhds_add_nhds_zero, nhds_mul_nhds_one, nhds_one_mul_nhds, nhds_zero_add_nhds, nonneg_nhds_iff, one_le_nhds_iff, tendsto_add, tendsto_finset_prod, tendsto_finset_sum, tendsto_list_prod, tendsto_list_sum, tendsto_mul, tendsto_mul_cocompact_nhds_zero, tendsto_mul_cofinite_nhds_zero, tendsto_mul_coprod_nhds_zero_inf_of_disjoint_cocompact, tendsto_mul_nhds_zero_of_disjoint_cocompact, tendsto_mul_nhds_zero_prod_of_disjoint_cocompact, tendsto_mul_prod_nhds_zero_of_disjoint_cocompact, tendsto_multiset_prod, tendsto_multiset_sum | 198 |
| Total | 221 |