ContinuousMap 📖 | CompData | 1535 mathmath: ContinuousMap.dense_setOf_contDiff, TopCat.isInducing_pullback_to_prod, AlgebraicGeometry.Scheme.toSpecΓ_apply, Sequential.homeoOfIso_apply, ContinuousMap.toLp_inj, TopCat.binaryCofan_isColimit_iff, ContinuousMap.ext_iff, ContinuousMap.isUniformInducing_equivBoundedOfCompact, DiscreteContAction.instDiscreteTopologyCarrierObjTopCatForget₂ContinuousMap, Circle.periodic_exp, AlgebraicGeometry.QuasiCompact.isCompact_preimage_singleton, AlgebraicGeometry.Scheme.fromSpecStalk_closedPoint, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_injective, exists_continuous_sum_one_of_isOpen_isCompact, SpectrumRestricts.nnreal_of_nonneg, AlgebraicGeometry.LocallyRingedSpace.stalkMap_hom_inv_assoc, ContinuousMap.addEquivBoundedOfCompact_apply, TopCat.pullbackIsoProdSubtype_hom_fst, ContinuousMap.instContinuousVAdd, TopologicalSpace.Opens.inclusion'_hom_apply, exists_continuous_forall_mem_convex_of_local, polynomialFunctions.eq_adjoin_X, AlgebraicGeometry.LocallyRingedSpace.residueFieldMap_comp, ContinuousMap.continuous, ContinuousMap.instContinuousEvalOfLocallyCompactPair, BumpCovering.eventuallyEq_one, bernsteinApproximation.apply_zero, TopologicalSpace.Opens.map_coe, AlgebraicGeometry.Scheme.Spec_map_stalkMap_fromSpecStalk, ContinuousMap.compactOpen_eq_iInf_induced, AlgebraicGeometry.Scheme.Cover.LocallyDirected.directed, Matrix.IsHermitian.isClosedEmbedding_cfcAux, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.stalk_iso, ProfiniteGrp.instReflectsIsomorphismsProfiniteForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, ContinuousMap.HomotopyRel.fst_eq_snd, IsSelfAdjoint.commute_cfcHom, ContinuousMap.constPi_apply, AlgebraicGeometry.QuasiCompact.isCompact_preimage, ContinuousMap.instIsTopologicalGroup, TopCat.GlueData.preimage_image_eq_image, ContinuousMap.yonedaPresheaf'_obj, AlgebraicGeometry.Scheme.Hom.denseRange, ContinuousMapZero.isEmbedding_toContinuousMap, AlgebraicGeometry.Scheme.isEmpty_pullback_iff, ContinuousMap.abs_mem_subalgebra_closure, TopCat.GlueData.π_surjective, ContinuousMap.compMonoidHom'_apply, ContinuousMap.hasBasis_nhds, ContinuousMap.HomotopyWith.coe_toContinuousMap, DeltaGenerated.topToDeltaGenerated_map_hom_hom_apply, AlgebraicGeometry.Scheme.Hom.closePoints_subset_preimage_closedPoints, TopCat.isOpenEmbedding_iff_comp_isIso, ContinuousMap.dist_lt_iff, Metric.exists_continuous_real_forall_closedEBall_subset, AlgebraicGeometry.coprodSpec_apply, AlgebraicGeometry.morphismRestrict_base_coe, AlgebraicGeometry.Scheme.Hom.fiberHomeo_apply, AlgebraicGeometry.surjectiveOnStalks_iff, ContinuousMap.instSubsingleton, ContinuousMap.HomotopyEquiv.refl_symm_apply, ContinuousMap.Homotopy.extend_apply_of_one_le, TopModuleCat.instPreservesLimitTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrierOfHasLimitOfModuleCatCompLinearMapForget, Circle.exp_arg, ContinuousMap.coeFn_toAEEqFun, ContinuousMap.exists_finite_approximation_of_mem_nhds_diagonal, AlgebraicGeometry.Scheme.affineBasisCover_is_basis, Profinite.forget_preservesLimits, CompactlyGenerated.homeoOfIso_apply, AlgebraicGeometry.range_eq_range_of_surjective, BumpCovering.toPartitionOfUnity_apply, AlgebraicGeometry.Scheme.Cover.isOpenMap_fromGlued, TopCat.coe_of_of, TopCat.Presheaf.stalkSpecializes_stalkPushforward, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_specStalkEquiv, AddCircle.homeomorphCircle'_apply_mk, AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint_x, TopCat.GlueData.open_image_open, ContinuousCohomology.I_obj_V_carrier, ContinuousMap.instIsScalarTower, ContinuousMap.attachBound_apply_coe, span_fourier_closure_eq_top, ContinuousMap.continuous_prodMk_const, Path.extend_extends, ContinuousMap.sup_apply, AlgebraicGeometry.Scheme.Hom.stalkMap_congr_point, AlgebraicGeometry.ValuativeCriterion.Existence.specializingMap, BoundedContinuousFunction.mkOfCompact_star, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_fromSpec, GenLoop.fromLoop_apply, ContinuousMap.toEquiv_homeoFnOfDiscrete, ContinuousMap.toLp_denseRange, AlgebraicGeometry.SheafedSpace.colimit_exists_rep, ODE.FunSpace.isUniformInducing_toContinuousMap, AlgebraicGeometry.Scheme.Hom.range_fiberι, TopologicalSpace.Opens.coe_inclusion', AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_invApp, TopologicalSpace.OpenNhds.inclusionMapIso_hom, AlgebraicGeometry.Scheme.Cover.iUnion_range, ContinuousMap.congr_arg, ContinuousMap.le_def, ContinuousMonoidHom.isInducing_toContinuousMap, AlgebraicGeometry.Scheme.Hom.mem_opensRange, Circle.exp_natCast_mul, Sequential.homeoOfIso_symm_apply, Path.Homotopic.map_lift, ContinuousMap.coe_addRight, AlgebraicGeometry.isCompact_iff_exists, AlgebraicGeometry.HasRingHomProperty.stalkMap, ContinuousMap.range_toLp, Real.tsum_eq_tsum_fourierIntegral_of_rpow_decay_of_summable, ContinuousMap.nsmul_comp, ContinuousMap.Homotopy.apply_zero_path, QuasispectrumRestricts.nnreal_iff, HomotopyGroup.symmAt_indep, hasSum_one_div_nat_pow_mul_fourier, ContinuousMapZero.instCanLift, ContinuousMap.dist_le_two_norm, ContinuousMap.isOpen_setOf_mapsTo, TopCommRingCat.instReflectsIsomorphismsTopCatForget₂SubtypeRingHomαContinuousCoeContinuousMapCarrier, ContinuousMap.norm_le, ContinuousMap.isUltrametricDist, PadicInt.norm_mahlerTerm, TopCat.uliftFunctorObjHomeo_symm_naturality_apply, BumpCovering.point_finite, ContinuousMap.norm_coe_le_norm, TopCat.uliftFunctorCompForgetIso_hom_app, deltaGenerated_eq_coinduced, ODE.FunSpace.range_toContinuousMap, ContinuousMap.notMem_idealOfSet, CompHausLike.coe_id, ContinuousMap.coe_intCast, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_hom_apply_asIdeal, ContinuousMap.dist_le, LocallyConstant.coe_comap_apply, AlgebraicGeometry.Scheme.OpenCover.finiteSubcover_f, AlgebraicGeometry.Scheme.stalkSpecializes_stalkMap, NonUnitalStarAlgHom.realContinuousMapZeroOfNNReal_apply_comp_toReal, Path.Homotopy.map_apply, AlgebraicGeometry.Scheme.Modules.germ_restrictStalkNatIso_inv_app, Polynomial.toContinuousMap_apply, ContinuousMap.specializes_coe, ContinuousMap.continuousMap_mem_subalgebra_closure_of_separatesPoints, ContinuousMap.mem_compactConvergence_entourage_iff, UnitAddTorus.mFourierSubalgebra_coe, AlgebraicGeometry.Scheme.stalkMap_congr_assoc, Path.ofLine_extend, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_surjective, AlgebraicGeometry.instIsGermInjectiveAtCoeContinuousMapCarrierCarrierCommRingCatHomTopCatBaseOfIsOpenImmersion, AlgebraicGeometry.Scheme.Pullback.SpecTensorTo_SpecOfPoint, ContinuousMap.toNNReal_neg_algebraMap, ContinuousMap.HomotopyLike.map_zero_left, ContinuousMap.Homotopy.evalAt_eq, AlgebraicGeometry.Scheme.hom_inv_apply, AlgebraicGeometry.Scheme.Hom.range_asFiberHom, ContinuousMap.vadd_comp, TopologicalSpace.Opens.map_obj, ContinuousMap.val_unitsLift_apply_apply, Subalgebra.SeparatesPoints.strongly, AlgebraicGeometry.Scheme.Hom.tendsto_cofinite_cofinite, PadicInt.mahlerTerm_apply, ContinuousAffineMap.coe_to_continuousMap, AlgebraicGeometry.Scheme.Hom.stalkSpecializes_stalkMap, ContinuousMap.coeNNRealReal_apply, AlgebraicGeometry.Scheme.Hom.coe_resLE_base, AlgebraicGeometry.IsAffineOpen.fromSpecStalk_closedPoint, UnitAddTorus.mFourierSubalgebra_closure_eq_top, BoundedContinuousFunction.toContinuousMapLinearMap_apply, ContinuousMap.coe_inf', TopCat.isOpenEmbedding_iff, AlgebraicGeometry.IsClosedImmersion.base_closed, AlgebraicGeometry.quasiCompact_iff, Profinite.effectiveEpi_tfae, TopologicalSpace.OpenNhds.inclusionMapIso_inv, TopCat.range_prod_map, LocallyConstant.toContinuousMapLinearMap_apply, TopModuleCat.instIsRightAdjointTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrier, Circle.isAddQuotientCoveringMap_exp, cfcHom_continuous, polynomialFunctions.starClosure_topologicalClosure, ContinuousMap.instContinuousMulOfLocallyCompactSpace, cfcL_apply, BumpCovering.support_toPOUFun_subset, SpectrumRestricts.nnreal_iff, ContinuousMapZero.isometry_toContinuousMap, AlgebraicGeometry.Scheme.Hom.stalkMap_congr_hom_assoc, ContinuousMap.div_comp, cfcHom_nonneg_iff, PartitionOfUnity.nonneg', gelfandStarTransform_naturality, ContinuousMap.exists_finite_sum_mul_approximation_of_mem_uniformity, AlgebraicGeometry.Scheme.Pullback.Triplet.isPullback_SpecMap_tensor, AlgebraicGeometry.Scheme.forget_map, TopCat.GlueData.isOpen_iff, AlgebraicGeometry.sigmaMk_mk, gelfandStarTransform_apply_apply, AlgebraicGeometry.Scheme.Pullback.Triplet.specTensorTo_base_snd, BoundedContinuousFunction.dist_toContinuousMap, TopologicalSpace.Fiber.sigmaIsoHom_inj, cfc_apply_mkD, AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr_point_assoc, BoundedContinuousFunction.toContinuousMapMonoidHom_apply, AlgebraicGeometry.Scheme.isoSpec_inv_preimage_zeroLocus, ContinuousMap.toLp_norm_le, ContinuousMap.coe_injective', Metric.exists_continuous_nnreal_forall_closedBall_subset, LocallyConstant.comapRingHom_apply_apply, Circle.exp_eq_exp, AlgebraicGeometry.IsPreimmersion.isEmbedding, GenLoop.homotopyTo_apply, Profinite.NobelingProof.spanFunctorIsoIndexFunctor_hom_app_hom_hom_apply_coe, TopCat.coequalizer_isOpen_iff, PartitionOfUnity.locallyFinite, TopCat.forget_preservesColimits, TopCat.GlueData.ι_fromOpenSubsetsGlue_apply, ContinuousMap.mem_idealOfSet, AlgebraicGeometry.Scheme.Hom.SpecMap_residueFieldMap_fromSpecResidueField_assoc, Path.extend_symm_apply, BoundedContinuousFunction.mkOfCompact_add, Polynomial.toAddCircle_X_pow_eq_fourier, ContinuousMap.mem_nhds_iff, Circle.exp_two_pi_mul_int, EMetric.exists_continuous_nnreal_forall_closedBall_subset, AlgebraicGeometry.IsOpenImmersion.iff_isIso_stalkMap, gelfandTransform_bijective, AlgebraicGeometry.Scheme.Cover.instIsIsoCommRingCatStalkMapFromGlued, AddCircle.scaled_exp_map_periodic, ContinuousMap.concatCM_left, LightProfinite.proj_comp_transitionMapLE', ContinuousMap.instStarModule, ContinuousMap.continuous_postcomp, AlgebraicGeometry.Scheme.Pullback.carrierEquiv_eq_iff, fourier_norm, ContinuousMap.piEquiv_symm_apply, cfcHom_isClosedEmbedding, ContinuousMap.continuous_iff_continuous_uniformOnFun, TopCat.pullback_topology, ContinuousMap.comp_const, TopCat.Presheaf.germ_stalkPullbackInv_assoc, AlgebraicGeometry.SpecToEquivOfLocalRing_apply_snd_coe, HomotopyGroup.isUnital_auxGroup, AlgebraicGeometry.Scheme.exists_affine_mem_range_and_range_subset, ProfiniteGrp.instFaithfulProfiniteForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, ContinuousMap.coev_apply, TotallyDisconnectedSpace.continuousMapEquivOfConnectedSpace_symm_apply_apply, exists_continuous_zero_one_of_isClosed, exists_continuous_forall_mem_convex_of_local_const, BoundedContinuousFunction.coe_toContinuousMapStarₐ, ProfiniteAddGrp.instFaithfulProfiniteForget₂ContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, ContinuousMap.HomotopyWith.apply_one, ContinuousMap.instNormedStarGroup, AlgebraicGeometry.IsOpenImmersion.isOpen_range, AlgebraicGeometry.Scheme.affineOpenCover_idx, ContinuousMap.norm_le_of_nonempty, ContinuousMap.instNontrivialOfNonempty, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.stalk_iso, AlgebraicGeometry.LocallyRingedSpace.iso_inv_base_hom_base_apply, AlgebraicGeometry.Scheme.Pullback.Triplet.snd_SpecTensorTo_apply, TopCat.pullbackFst_apply, TopologicalSpace.Opens.mem_comap, AlgebraicGeometry.PresheafedSpace.stalkMap.stalkSpecializes_stalkMap, CompHausLike.LocallyConstant.locallyConstantIsoContinuousMap_inv_apply, LightCondSet.topCatAdjunctionUnit_val_app_apply, ProfiniteAddGrp.instPreservesLimitsProfiniteForget₂ContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, FundamentalGroup.map_apply, TopCat.colimit_topology, Profinite.epi_iff_surjective, AlgebraicGeometry.Scheme.presieve₀_mem_precoverage_iff, ContinuousMap.coeFnAddMonoidHom_apply, TopologicalSpace.Opens.isOpenEmbedding_obj_top, PartitionOfUnity.sum_eq_one', ContinuousMap.HomotopyRel.refl_apply, AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToΓ_ΓToStalk, AlgebraicGeometry.isIso_iff_isIso_stalkMap, AlgebraicGeometry.LocallyRingedSpace.stalkMap_inv_hom, ContinuousMap.continuous_compactOpen, ContinuousMap.Homotopy.ulift_apply, TopCat.isOpenEmbedding_iff_isIso_comp', ContinuousMap.piMap_apply, GenLoop.loopHomeo_apply, UnitAddTorus.mFourierCoeff_toLp, ContinuousMap.coe_homeoFnOfDiscrete, AlgebraicGeometry.Scheme.Pullback.residueFieldCongr_inv_residueFieldMap_ofPoint, AlgebraicGeometry.IsOpenImmersion.range_pullbackSnd, AlgebraicGeometry.Scheme.Hom.isDiscrete_preimage_singleton, algebraMap_apply, BoundedContinuousFunction.mkOfCompact_zero, TopCat.pullbackSnd_apply, AlgebraicGeometry.Scheme.IdealSheafData.range_glueDataObjι_ι_eq_support_inter, LightProfinite.isClosedMap, AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr, Path.truncate_self, AlgebraicGeometry.IsOpenImmersion.range_pullback_fst_of_right, cfcHom_le_iff, Homeomorph.continuousMapCongr_symm_apply, cfcHom_id, AlgebraicGeometry.Scheme.Hom.coe_resLE_apply, ContinuousMap.coe_vadd, AlgebraicGeometry.pointEquivClosedPoint_apply_coe, ContinuousMap.inf_apply, ContinuousMap.dist_apply_le_dist, Path.continuous_extend, PartitionOfUnity.exists_finset_nhds, Path.extend_trans_of_le_half, TopCat.isIso_iff_isHomeomorph, PadicInt.fwdDiff_tendsto_zero, Continuous.pathExtend, AlgebraicGeometry.Scheme.Opens.germ_stalkIso_inv, ContinuousMap.hasFiniteIntegral_of_bound, AlgebraicGeometry.Scheme.range_fromSpecStalk, ContinuousMap.norm_eq_iSup_norm, TopCat.prod_topology, PartitionOfUnity.IsSubordinate.continuous_finsum_smul, ContinuousCohomology.I_obj_ρ_apply, ContinuousMap.toNNReal_algebraMap, CondensedSet.topCatAdjunctionCounit_bijective, ContinuousMap.uniformContinuous_comp_left, spectrum.gelfandTransform_eq, Homeomorph.continuousMapCongr_apply, AlgebraicGeometry.coprodMk_inl, CondensedSet.topCatAdjunctionCounit_hom_apply, ContinuousMap.spectrum_eq_preimage_range, PadicInt.mahlerSeries_apply, Path.extend_apply, AlgebraicGeometry.Scheme.Pullback.Triplet.hy, AlgebraicGeometry.LocallyRingedSpace.stalkMap_inv_hom_assoc, TopCat.forget_preservesLimitsOfSize, TopCat.sigmaIsoSigma_inv_apply, ContinuousMap.continuous_toNNReal, ContinuousMap.Homotopy.pathExtend_evalAt, CompHausLike.homeoOfIso_symm_apply, AlgebraicGeometry.Scheme.Pullback.carrierEquiv_symm_fst, DiscreteQuotient.map_comp_proj, Homeomorph.continuousMapOfUnique_apply, AlgebraicGeometry.Scheme.Hom.asFiberHom_fiberι_assoc, CompHausLike.isClosedMap, ContinuousLinearMap.const_apply_apply, WeakDual.CharacterSpace.continuousMapEval_bijective, AlgebraicGeometry.PresheafedSpace.GlueData.pullback_base, AlgebraicGeometry.Scheme.Hom.app_appIso_inv_assoc, fourier_one, ContinuousMap.coeFnAlgHom_apply, FintypeCat.toProfinite_map_hom_hom_apply, TopCat.pullbackIsoProdSubtype_inv_fst_assoc, ContinuousMap.coeFnRingHom_apply, AlgebraicGeometry.Scheme.Pullback.range_fst_comp, Path.uniformContinuous_extend_left, TopologicalSpace.OpenNhds.op_map_id_obj, continuousMap_mem_polynomialFunctions_closure, AlgebraicGeometry.Scheme.isoSpec_inv_image_zeroLocus, AlgebraicGeometry.Scheme.IdealSheafData.range_glueDataObjι_ι, HomotopyGroup.transAt_indep, AlgebraicGeometry.Scheme.Modules.germ_restrictStalkNatIso_hom_app, ContinuousMap.Homotopy.compContinuousMap_apply, ContinuousMap.dist_lt_of_dist_lt_modulus, ZeroAtInftyContinuousMap.ContinuousMap.liftZeroAtInfty_apply_toFun, StarAlgHom.realContinuousMapOfNNReal_apply, ContinuousMap.idealOfSet_closed, AlgebraicGeometry.morphismRestrict_base, IsCoveringMap.injective_path_homotopic_map, gelfandStarTransform_symm_apply, PadicInt.coe_addChar_of_value_at_one, AlgebraicGeometry.Scheme.toSpecΓ_preimage_zeroLocus, LightProfinite.effectiveEpi_iff_surjective, AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.imageBasicOpen_image_open, PadicInt.mahlerSeries_apply_nat, AlgebraicGeometry.Scheme.Hom.quasiFiniteAt_comp_iff_of_isOpenImmersion, Polynomial.toAddCircle.integrable, ContinuousMap.smul_apply, ContinuousMap.instT1Space, TopologicalSpace.Opens.inclusion'_top_functor, ContinuousMap.coe_comp, fourier_zero, AlgebraicGeometry.Scheme.Cover.isOpenEmbedding_fromGlued, ContinuousMap.pow_apply, fourier_neg', AlgebraicGeometry.coe_opensRestrict_symm_apply, PartitionOfUnity.coe_finsupport, ContinuousMap.coe_sub, ContinuousMap.instPseudoMetrizableSpace, AlgebraicGeometry.Scheme.Hom.isCompact_preimage_singleton, GenLoop.instContinuousEval, AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_ideal, ContinuousMap.instIsTopologicalAddGroup, AlgebraicGeometry.Scheme.Pullback.Triplet.Spec_map_tensor_isPullback, UniformFun.isometry_ofFun_continuousMap, PartitionOfUnity.exists_finset_nhds_support_subset, ContinuousMap.hasBasis_compactConvergenceUniformity, AlgebraicGeometry.Scheme.Cover.covers, alexDiscEquivPreord_inverse_map, WeakDual.CharacterSpace.homeoEval_naturality, ContinuousMap.coe_const', AlgebraicGeometry.Scheme.Hom.stalkMap_congr_point_assoc, TopologicalSpace.Opens.map_functor_eq, TopCommRingCat.forgetToTopCatTopologicalRing, Path.Homotopy.eval_apply, BoundedContinuousFunction.toContinuousMapAddMonoidHom_apply, AlgebraicGeometry.Scheme.stalkMap_congr_point_assoc, ContinuousMap.homeoFnOfDiscrete_symm_apply, AlgebraicGeometry.Scheme.GlueData.isOpen_iff, ContinuousMap.coe_restrict, Circle.exp_two_pi, ContinuousAddMonoidHom.range_toContinuousMap, AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr_assoc, Subalgebra.separatesPoints_monotone, ContinuousMap.isUnit_iff_forall_isUnit, ContinuousMap.Homotopy.apply_one_path, PartitionOfUnity.sum_le_one', AlgebraicGeometry.QuasiCompactCover.isCompactOpenCovered_of_isCompact, ContinuousMap.one_apply, ContinuousMap.inseparable_coe, UnitAddTorus.mFourier_add, AlgebraicGeometry.PresheafedSpace.stalkMap.stalkSpecializes_stalkMap_apply, ContinuousMap.lt_def, AlgebraicGeometry.Scheme.Hom.mem_preimage, AlgebraicGeometry.Scheme.Spec_map_stalkMap_fromSpecStalk_assoc, BumpCovering.le_one, AlgebraicGeometry.Scheme.Hom.isConstructible_preimage, AlgebraicGeometry.LocallyRingedSpace.isLocalHomStalkMap, ContinuousMap.equivFnOfDiscrete_apply, AlgebraicGeometry.IsImmersion.isLocallyClosed_range, ContinuousMap.HomotopyRel.compContinuousMap_apply, AlgebraicGeometry.Scheme.Γevaluation_naturality_apply, CompHausLike.finiteCoproduct.isOpenEmbedding_ι, IsCoveringMap.injective_path_homotopic_mapFn, ContinuousMap.coe_mulRight, ContinuousMap.compactOpen_eq, BoundedContinuousFunction.norm_toContinuousMap_eq, CompHausLike.Sigma.isOpenEmbedding_ι, AlgebraicGeometry.ExistsHomHomCompEqCompAux.exists_index, Path.Homotopic.map, Circle.exp_sub, AlgebraicGeometry.LocallyRingedSpace.coe_toΓSpecSheafedSpace_hom_base_hom_apply_asIdeal, TopCat.range_pullback_map, AlgebraicGeometry.Scheme.Cover.exists_lift_trans_eq, NormedSpace.exp_continuousMap_eq, UnitAddTorus.mFourier_zero, ContinuousMap.continuousOn_mkD_of_uncurry, AlgebraicGeometry.Spec_map_localization_isIso, AlgebraicGeometry.Scheme.stalkClosedPointTo_fromSpecStalk, PartitionOfUnity.sum_eq_one, AlgebraicGeometry.Scheme.coe_homeoOfIso_symm, AlgebraicGeometry.ProjectiveSpectrum.Proj.isLocalization_atPrime, AlgebraicGeometry.Scheme.stalkMap_hom_inv_assoc, bernstein.variance, AlgebraicGeometry.Scheme.IdealSheafData.range_subschemeι, bernstein_apply, TopologicalSpace.productOfMemOpens_isEmbedding, gelfandTransform_map_star, polynomialFunctions.starClosure_eq_adjoin_X, AlgebraicGeometry.PresheafedSpace.GlueData.ι_image_preimage_eq, LocallyConstant.coe_comap, AlgebraicGeometry.PresheafedSpace.stalkMap.congr, Path.Homotopic.map_trans_evalAt, AlgebraicGeometry.Scheme.Hom.isClosedMap, AlgebraicGeometry.Scheme.Hom.isLocallyClosed_range, ContinuousMap.isEmbedding_sigmaMk_comp, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec_assoc, TopCat.uliftFunctorObjHomeo_naturality_apply, TopCat.homeoOfIso_apply, AlgebraicGeometry.morphismRestrict_appLE, UnitAddTorus.coeFn_mFourierLp, Stonean.epi_iff_surjective, AlgebraicGeometry.IsClosedImmersion.iff_isPreimmersion, ContinuousMap.aeStronglyMeasurable_restrict_mkD_restrict_of_uncurry, GenLoop.ext_iff, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec, ContinuousMap.dist_lt_iff_of_nonempty, ContinuousMap.uncurry_apply, exists_continuous_one_zero_of_isCompact, AlgebraicGeometry.Scheme.Hom.apply_mem_image_iff, AlgebraicGeometry.Scheme.Hom.asFiberHom_apply, MeasureTheory.ProbabilityMeasure.continuous_iff_forall_continuousMap_continuous_integral, ContinuousMap.instContinuousMapClass, Circle.exp_neg, ContinuousMap.compStarAlgHom_comp, BumpCovering.toPartitionOfUnity_eq_mul_prod, ProfiniteAddGrp.instIsTopologicalAddGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousAddMonoidHomToProfiniteContinuousMap, ContinuousMap.neg_comp, TopCat.Presheaf.germToPullbackStalk_stalkPullbackHom, Path.truncate_zero_zero, ContinuousMap.linearIsometryBoundedOfCompact_symm_apply, Real.tsum_eq_tsum_fourier_of_rpow_decay_of_summable, AlgebraicGeometry.genericPoint_eq_of_isOpenImmersion, AlgebraicGeometry.Scheme.homeoOfIso_apply, ContinuousMap.restrictPreimage_apply, ContinuousMap.compStarAlgHom'_comp, ContinuousMap.ideal_isMaximal_iff, ContinuousMap.instStarOrderedRingOfContinuousSqrt, AlgebraicGeometry.Scheme.Opens.germ_stalkIso_inv_assoc, AlgebraicGeometry.formallySmooth_stalkMap_iff, TopCat.nonempty_isLimit_iff_eq_induced, UnitAddTorus.mFourier_neg, AlgebraicGeometry.isIso_stalkMap_coprodSpec, ContinuousMap.addUnitsLift_apply_neg_apply, AlgebraicGeometry.LocallyRingedSpace.residue_comp_residueFieldMap_eq_stalkMap_comp_residue, exists_continuous_nonneg_pos, ContinuousMap.sup_mem_closed_subalgebra, ContinuousFunctionalCalculus.exists_cfc_of_predicate, ContinuousMap.periodic_tsum_comp_add_zsmul, Profinite.IndexFunctor.surjective_π_app, ContinuousMap.evalCLM_apply, ContinuousMap.val_unitsLift_symm_apply_apply, AlgebraicGeometry.Scheme.instIsIsoCommRingCatResidueFieldMapOfIsOpenImmersion, BoundedContinuousFunction.mkOfCompact_apply, AlgebraicGeometry.Scheme.instIsOverMapResidueFieldMapOverInferInstanceOverClass, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.image_preimage_is_empty, ContinuousMap.linearIsometryBoundedOfCompact_of_compact_toEquiv, ContinuousMap.Homotopy.extend_apply_coe, LocallyConstant.toContinuousMap_injective, ContinuousMap.Homotopy.evalAt_apply, Profinite.NobelingProof.iso_map_bijective, ContinuousMap.HomotopyEquiv.trans_apply, ContinuousMap.toLp_def, TopCat.id_app, AlgebraicGeometry.Scheme.Γevaluation_naturality_assoc, AlgebraicGeometry.Scheme.Pullback.carrierEquiv_symm_snd, ContinuousMap.prodMap_apply, IsCoveringMap.monodromy_map, ContinuousMap.coeFnLinearMap_apply, TopCat.hasLimit_iff_small_sections, AlgebraicGeometry.isCompl_range_inl_inr, PartitionOfUnity.exists_isSubordinate_of_locallyFinite_t2space, LightCondensed.isoFinYonedaComponents_inv_comp, ContinuousMap.inv_comp, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app, cfc_def, Path.Homotopic.Quotient.mk_map, fourier_coe_apply, ContinuousMap.coe_zero, TopCat.piIsoPi_inv_π_apply, GenLoop.continuous_fromLoop, LocallyConstant.toContinuousMapMonoidHom_apply, ContinuousMap.instVAddCommClass, AlgebraicGeometry.Scheme.Pullback.range_map, fourierSubalgebra_separatesPoints, AlgebraicGeometry.ProjIsoSpecTopComponent.fromSpec_toSpec, AlgebraicGeometry.SurjectiveOnStalks.isEmbedding_pullback, AlexDisc.forgetToTop_faithful, ContinuousMap.sigmaEquiv_symm_apply, AlgebraicGeometry.Scheme.Hom.isSpectralMap, TopologicalSpace.productOfMemOpens_injective, AlgebraicGeometry.mem_range_iff_of_surjective, ContinuousMap.nnnorm_lt_iff, StarAlgHom.realContinuousMapOfNNReal_apply_comp_toReal, CondensedSet.topCatAdjunctionUnit_val_app_apply, IsUltrametricDist.norm_fwdDiff_iter_apply_le, ContinuousMap.map_specializes, TopCat.GlueData.f_open, Circle.exp_inj, AlgebraicGeometry.Scheme.Hom.isLocallyConstructible_image, BumpCovering.locallyFinite, ContinuousMapZero.toContinuousMapCLM_apply, ContinuousMap.prodSwap_apply, ContinuousMap.instIsOrderedAddMonoid, AlgebraicGeometry.LocallyRingedSpace.stalkMap_inv_hom_apply, Path.extend_of_one_le, ContinuousMap.exists_mem_subalgebra_near_continuousMap_of_separatesPoints, ContinuousMap.coe_addLeft, AlgebraicGeometry.Scheme.stalkMap_congr_hom_assoc, AlgebraicGeometry.Scheme.Opens.germ_stalkIso_hom, MeasureTheory.FiniteMeasure.continuous_iff_forall_continuousMap_continuous_lintegral, Circle.exp_add_two_pi, ContinuousMap.abs_apply, Path.image_extend_of_subset, AlgebraicGeometry.Scheme.stalkSpecializes_stalkMap_apply, has_antideriv_at_fourier_neg, UnitAddTorus.mFourier_norm, GenLoop.toLoop_apply, ContinuousMap.exists_finite_sum_const_indicator_approximation_of_mem_nhds_diagonal, TopologicalSpace.OpenNhds.map_id_obj_unop, ODE.FunSpace.toContinuousMap_apply_eq_apply, ContinuousMap.comp_apply, TopologicalSpace.productOfMemOpens_isInducing, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app', ContinuousMonoidHom.toContinuousMap_injective, ContinuousAt.pathExtend, TopCat.isOpenEmbedding_iff_comp_isIso', ContinuousMap.HomotopicRel.equivalence, Circle.invOn_arg_exp, ContinuousMap.coe_injective, TopCat.isOpenEmbedding_f_zeroHypercover, TopologicalSpace.Opens.isOpenEmbedding, ContinuousMap.equivBoundedOfCompact_apply, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_zeroLocus, TopCat.GlueData.range_fromOpenSubsetsGlue, PartitionOfUnity.finsum_smul_mem_convex, exists_continuous_zero_one_of_isCompact', TopCat.coe_id, AlgebraicGeometry.Scheme.GlueData.ι_eq_iff, AlgebraicGeometry.FormallyUnramified.instIsSeparableCarrierResidueFieldCoeContinuousMapCarrierCarrierCommRingCatHomTopCatBaseOfLocallyOfFiniteType, ContinuousMap.smul_comp, FintypeCat.toLightProfinite_map_hom_hom_apply, nonneg_iff_isSelfAdjoint_and_spectrumRestricts, NNReal.ContinuousMap.canLift, HomotopyGroup.mul_spec, TopCat.uliftFunctorCompForgetIso_inv_app, ContinuousMap.coe_smul', AlgebraicGeometry.AffineSpace.isOpenMap_over, AlgebraicGeometry.surjective_iff, TopologicalSpace.Fiber.sigmaIsoHom_apply, ContinuousMap.nnnorm_smul_const, ContinuousMap.yonedaPresheaf_obj, ContinuousMap.adjoin_id_eq_span_one_union, HSpace.hmul_e_e, PartitionOfUnity.nonneg, hasDerivAt_fourier_neg, Profinite.exists_isClopen_of_cofiltered, ContinuousMap.unitsLift_apply_inv_apply, Metric.exists_continuous_real_forall_closedBall_subset, AlgebraicGeometry.Scheme.SpecMap_stalkMap_fromSpecStalk_assoc, fourier_eval_zero, Stonean.forget.preservesLimits, Matrix.IsHermitian.cfcAux_apply, AlgebraicGeometry.Scheme.singleton_mem_precoverage_iff, ContinuousMap.nhds_compactOpen_eq_iInf_nhds_induced, ContinuousMap.toNNReal_one, Path.extend_range, Real.Angle.toCircle_coe, AlgebraicGeometry.Scheme.Hom.isOpenMap, ContinuousMap.toLp_norm_eq_toLp_norm_coe, GenLoop.fromLoop_symm_toLoop, LocallyConstant.toContinuousMapAddMonoidHom_apply, ContinuousMap.sigma_apply, mahler_natCast_eq, ContinuousMap.sup_mem_subalgebra_closure, AlgebraicGeometry.Scheme.Pullback.Triplet.hx, ContinuousMap.div_apply, ContinuousMap.vadd_apply, TopCat.GlueData.MkCore.t_inv, AlgebraicGeometry.isOpenImmersion_iff_stalk, fourierCoeff_toLp, AlgebraicGeometry.LocallyRingedSpace.Hom.prop, AlgebraicGeometry.SurjectiveOnStalks.surj_on_stalks, AlgebraicGeometry.Scheme.Hom.stalkSpecializes_stalkMap_assoc, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_invApp_assoc, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_invApp, ContinuousAddMonoidHom.isClosedEmbedding_toContinuousMap, ContinuousMap.val_addUnitsLift_apply_apply, TopCat.isClosed_iff_of_isColimit, ContinuousMap.homeoFnOfDiscrete_apply, CompHausLike.LocallyConstant.locallyConstantIsoContinuousMap_hom, AlgebraicGeometry.SurjectiveOnStalks.stalkMap_surjective, Homeomorph.continuousMapOfUnique_symm_apply, TopCat.pullbackIsoProdSubtype_inv_snd_apply, ContinuousMap.instContinuousConstVAdd, AlgebraicGeometry.PresheafedSpace.stalkMap.isIso, PartitionOfUnity.locallyFinite', ContinuousMap.coe_neg, ContinuousMap.coe_nsmul, exists_polynomial_near_continuousMap, Path.isUniformEmbedding_coe, ContinuousMap.inf_mem_subalgebra_closure, ContinuousMap.continuous_const', TopCat.GlueData.fromOpenSubsetsGlue_isOpenEmbedding, AlgebraicGeometry.Scheme.Hom.stalkMap_hom_inv, Metric.exists_continuous_nnreal_forall_closedEBall_subset, AlgebraicGeometry.Scheme.IdealSheafData.support_comap, ContinuousLinearMap.compLeftContinuous_apply, TopologicalSpace.Opens.set_range_inclusion', AlgebraicGeometry.Scheme.stalkMap_congr_hom, ContinuousMap.nnnorm_lt_iff_of_nonempty, ContinuousMap.inf_mem_closed_subalgebra, AlgebraicGeometry.Scheme.Pullback.range_snd_comp, ContinuousMap.continuous_iff_continuous_uniformFun, AlgebraicGeometry.LocallyRingedSpace.GlueData.ι_jointly_surjective, Circle.exp_add, ContinuousMap.sigmaMk_apply, AlgebraicGeometry.range_eq_univ, BumpCovering.nonneg', ContinuousMap.tendsto_iff_tendstoUniformly, AlgebraicGeometry.SpecToEquivOfLocalRing_apply_fst, AlgebraicGeometry.Scheme.Hom.comp_apply, CocompactMap.coe_toContinuousMap, ContinuousMap.exists_mem_subalgebra_near_continuous_of_isCompact_of_separatesPoints, ContinuousMap.coe_equivFnOfDiscrete, AlgebraicGeometry.Scheme.Hom.isOpenEmbedding, LightProfinite.surjective_transitionMapLE, TopCat.pullbackIsoProdSubtype_inv_fst, IsSelfAdjoint.sq_spectrumRestricts, WeakDual.CharacterSpace.compContinuousMap_apply, AlgebraicGeometry.Spec.map_apply, AlgebraicGeometry.pointOfClosedPoint_apply, AlgebraicGeometry.PresheafedSpace.GlueData.ι_isOpenEmbedding, ContinuousMap.compAddMonoidHom'_apply, continuous_cfcHomSuperset_left, ContinuousMap.sum_apply, AlgebraicGeometry.Scheme.Hom.isEmbedding, AlgebraicGeometry.sigmaι_eq_iff, PartitionOfUnity.sum_finsupport_smul_eq_finsum, ContinuousCohomology.I_map_hom, BoundedContinuousFunction.mkOfCompact_neg, LocallyConstant.comapₗ_apply_apply, isOpen_deltaGenerated_iff, ContinuousMap.zpow_apply, CompHausLike.mono_iff_injective, AlgebraicGeometry.Scheme.stalkMap_comp, ContinuousMap.notMem_setOfIdeal, TopModuleCat.freeMap_map, ContinuousMap.instCompleteSpaceOfCompactlyCoherentSpace, bernsteinApproximation.apply_one, AlgebraicGeometry.IsOpenImmersion.range_pullback_to_base_of_left, TopCat.coinduced_of_isColimit, ZeroAtInftyContinuousMap.ContinuousMap.liftZeroAtInfty_symm_apply, Circle.leftInverse_exp_arg, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_invApp, bernstein_nonneg, AlgebraicGeometry.Scheme.IdealSheafData.map_vanishingIdeal, AlgebraicGeometry.Scheme.Hom.stalkMap_inv_hom_assoc, BumpCovering.exists_finset_toPartitionOfUnity_eventuallyEq, CompactExhaustion.hasAntitoneBasis_compactConvergenceUniformity, ContinuousMap.toUniformOnFun_toFun, PartitionOfUnity.locallyFinite_tsupport, AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.coequalizer_π_stalk_isLocalHom, LightProfinite.forget_reflectsIsomorphisms, CompHausLike.forget_reflectsIsomorphisms, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_apply_eq, ContinuousMap.inv_apply, ContinuousMap.coe_zsmul, BumpCovering.locallyFinite_tsupport, PartitionOfUnity.continuous_finsum_smul, AlgebraicGeometry.LocallyRingedSpace.Γevaluation_naturality_apply, ContinuousMap.inf'_apply, ContinuousMap.instIsTopologicalSemiringOfLocallyCompactSpace, curveIntegralFun_def', Topology.IsGeneratedBy.isOpen_iff, ContinuousMap.instCStarRing, ContinuousAddMonoidHom.isInducing_toContinuousMap, Condensed.isoFinYonedaComponents_inv_comp, AlgebraicGeometry.Scheme.Hom.residueFieldMap_congr, ContinuousMap.exists_finite_sum_const_mulIndicator_approximation_of_mem_nhds_diagonal, TopCat.pullbackIsoProdSubtype_hom_snd, ContinuousMapZero.norm_def, AlgebraicGeometry.Scheme.Hom.map_mem_image_iff, cfc_eq_cfcL_mkD, hasDerivAt_fourier, ContinuousMap.instSMulCommClass_2, TopologicalSpace.Opens.adjunction_counit_map_functor, ContinuousMap.instT3Space, AlgebraicGeometry.coprodSpec_coprodMk, ContinuousMap.HomotopyWith.extendProp, fourier_apply, ContinuousMap.aeStronglyMeasurable_mkD_restrict_of_uncurry, ContinuousMap.Homotopy.curry_apply, DeltaGeneratedSpace.isOpen_iff, AlgebraicGeometry.Scheme.Hom.injective, ContinuousMap.tendsto_iff_forall_isCompact_tendstoUniformlyOn, cfcHomSuperset_apply, ContinuousMapZero.map_zero', TopCat.pullbackIsoProdSubtype_inv_snd, range_cfc_eq_range_cfcHom, AlgebraicGeometry.Scheme.Hom.asFiberHom_fiberι, TopCat.hasColimit_iff_small_colimitType, Circle.argEquiv_symm_apply, AddCircle.toCircle_apply_mk, ContinuousMap.continuous_coev, TopCat.GlueData.fromOpenSubsetsGlue_injective, TopologicalSpace.Opens.adjunction_counit_app_self, AlgebraicGeometry.LocallyOfFiniteType.stalkMap, Trivialization.proj_clift, Profinite.IndexFunctor.map_comp_π_app, ContinuousMap.instContinuousSMul, ContinuousMap.continuous_restrict, TopologicalSpace.Opens.mem_map, AlgebraicGeometry.locallyQuasiFinite_iff_isDiscrete_preimage_singleton, AlgebraicGeometry.Scheme.IsLocallyDirected.ι_eq_ι_iff, ContinuousMap.Homotopy.extend_apply_of_mem_I, BumpCovering.toFun_eq_coe, ContinuousMap.toNNReal_mul_add_neg_mul_add_mul_neg_eq, GenLoop.toLoop_apply_coe, LightCondSet.topCatAdjunctionCounit_bijective, CompactlyGenerated.homeoOfIso_symm_apply, ContinuousMap.continuous_uncurry, ContinuousMap.curry_apply, AlgebraicGeometry.Scheme.Pullback.Triplet.specTensorTo_base_fst, AlgebraicGeometry.compactSpace_iff_exists, ContinuousMap.comp_one, PadicInt.hasSum_mahlerSeries, AlgebraicGeometry.Scheme.stalkMap_congr_point, ContinuousMapZero.toContinuousMapHom_toNNReal, AlgebraicGeometry.ProjectiveSpectrum.Proj.mk_mem_toSpec_base_apply, SpectralMap.coe_comp_continuousMap, TopCat.range_pullback_to_prod, AlgebraicGeometry.IsAffineOpen.comap_primeIdealOf_appLE, TopCat.GlueData.ι_isOpenEmbedding, AlgebraicGeometry.Scheme.stalkMap_hom_inv, AlgebraicGeometry.Scheme.toSpecΓ_image_zeroLocus, ContinuousMap.image_coev, ContinuousOpenMap.coe_toContinuousMap, AlgebraicGeometry.LocallyRingedSpace.evaluation_naturality, AlgebraicGeometry.isImmersion_iff, fourierSubalgebra_coe, ContinuousMap.comp_zero, ContinuousMap.zpow_comp, TopCat.pullback_fst_image_snd_preimage, Polynomial.toAddCircle_monomial_eq_smul_fourier, TopModuleCat.instPreservesLimitsOfShapeTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrierOfHasLimitsOfShapeOfModuleCatForgetLinearMap, ContinuousOn.continuous_restrict_iff_continuous_uniformOnFun, GenLoop.loopHomeo_symm_apply, ContinuousMap.zero_apply, Metric.exists_continuous_ennreal_forall_closedEBall_subset, EMetric.exists_continuous_real_forall_closedBall_subset, AlgebraicGeometry.Scheme.stalkMap_hom_inv_apply, TopCat.continuous_iff_of_isColimit, BumpCovering.ind_apply, Real.probChar_apply', ContinuousMap.subalgebra_topologicalClosure_eq_top_of_separatesPoints, Topology.WithGeneratedByTopology.continuous_from_iff, lightProfiniteToLightCondSetIsoTopCatToLightCondSet_hom_app_val_app_apply, ContinuousMap.norm_lt_iff, ContinuousMap.norm_lt_iff_of_nonempty, ContinuousMap.coe_add, ContinuousMap.coe_id, cfcHom_eq_cfc_extend, AlgebraicGeometry.Scheme.Hom.stalkSpecializes_stalkMap_apply, Path.continuous_uncurry_extend_of_continuous_family, AlgebraicGeometry.LocallyRingedSpace.isLocalHomStalkMap', AlgebraicGeometry.LocallyRingedSpace.stalkMap_hom_inv, TopCat.instIsLeftAdjointForgetContinuousMapCarrier, TopCat.pullbackIsoProdSubtype_inv_fst_apply, AlgebraicGeometry.Scheme.Hom.exists_mem_and_isIso_morphismRestrict_toNormalization, ContinuousMap.HomotopyLike.map_one_left, ContinuousMap.star_apply, CompHausLike.const_comp, exists_continuous_zero_one_of_isCompact, TopCat.piIsoPi_hom_apply, ContinuousMap.piEquiv_apply, ContinuousMap.aeStronglyMeasurable_restrict_mkD_of_uncurry, AlgebraicGeometry.Scheme.descResidueField_stalkClosedPointTo_fromSpecResidueField, ContinuousMap.realToNNReal_apply, AlexDisc.Iso.mk_inv, CompHausLike.finiteCoproduct.ι_injective, ContinuousMap.toLp_injective, Circle.exp_zero, ContinuousMap.sigmaEquiv_apply, AlgebraicGeometry.isDominant_iff, AlgebraicGeometry.Flat.generalizingMap, AlgebraicGeometry.Scheme.Hom.fiberι_asFiber, TopCat.GlueData.MkCore.t_id, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.c_iso, ContinuousMap.instIsBoundedSMul, AlgebraicGeometry.IsOpenImmersion.range_pullback_snd_of_left, AlgebraicGeometry.IsOpenImmersion.instIsIsoCommRingCatStalkMap, AlgebraicGeometry.isPreimmersion_iff, AlgebraicGeometry.Scheme.AffineCover.covers, PadicInt.hasSum_mahler, UnitAddTorus.mFourierSubalgebra_separatesPoints, ContinuousMap.isHomeomorph_coe, ContinuousMap.coe_toLp, Commute.cfcHom, AlgebraicGeometry.Scheme.Hom.Spec_map_residueFieldMap_fromSpecResidueField_assoc, AlgebraicGeometry.Scheme.isLocalHom_stalkClosedPointTo', ContinuousMap.instT2Space, AlgebraicGeometry.IsFinite.finite_preimage_singleton, TopCat.Presheaf.germ_stalkPullbackInv, fourierCoeff_eq_intervalIntegral, ContinuousMap.instContinuousEvalConst, ContinuousMap.evalStarAlgHom_apply, ContinuousMap.piComparison_fac, ContinuousMap.ideal_gc, AlgebraicGeometry.IsAffineOpen.primeIdealOf_eq_map_closedPoint, ContinuousMap.canLift, AlgebraicGeometry.Scheme.IdealSheafData.range_glueDataObjι, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app_assoc, ContinuousMap.coe_apply, Polynomial.aeval_continuousMap_apply, ContinuousMap.subsingleton_subalgebra, ContinuousMap.nonUnitalStarAlgebraAdjoin_id_subset_ker_evalStarAlgHom, cfc_apply, ContinuousMap.prod_apply, TopCat.GlueData.preimage_range, HomotopyGroup.one_def, alexDiscEquivPreord_unitIso, ContinuousMap.setOfTop_eq_univ, ContinuousMap.mkD_apply_of_continuousOn, AlgebraicGeometry.IsOpenImmersion.range_pullback_to_base_of_right, TopCat.isOpenEmbedding_iff_isIso_comp, ContinuousMap.coe_sup', CompHaus.effectiveEpi_tfae, LightProfinite.instPreservesLimitsOfShapeOppositeNatForgetContinuousMapCarrierToTopAndTotallyDisconnectedSpaceSecondCountableTopology, ContinuousMap.continuous_uncurry_of_continuous, TopologicalSpace.Opens.functor_map_eq_inf, ContinuousMap.Homotopy.extend_of_mem_I, ContinuousMap.HomotopyEquiv.coe_invFun, ContinuousMap.instSMulCommClass_1, ContinuousMap.val_addUnitsLift_symm_apply_apply, ContinuousMap.coe_zpow, ContinuousMap.instIsTopologicalRingOfLocallyCompactSpace, AlgebraicGeometry.Scheme.Pullback.Triplet.fst_SpecTensorTo_apply, ContinuousMap.toNNReal_apply, CompactlySupportedContinuousMap.coe_toContinuousMap, polynomialFunctions_coe, ContinuousMap.neg_norm_le_apply, ContinuousMonoidHom.isEmbedding_toContinuousMap, Polynomial.fourierCoeff_toAddCircle_natCast, ContinuousMap.coe_inf, ContinuousMap.spectrum_eq_range, fourierCoeffOn_of_hasDerivAt_Ioo, AlexDisc.coe_forgetToTop, TopologicalSpace.OpenNhds.isOpenEmbedding, ContinuousMap.isUniformEmbedding_toUniformOnFunIsCompact, TopModuleCat.forget₂_TopCat_obj, Polynomial.toContinuousMapAlgHom_apply, ContinuousMap.tendsto_iff_tendstoLocallyUniformly, AlgebraicGeometry.IsClosedImmersion.isClosedEmbedding, Path.truncate_zero_one, CompHausLike.homeoOfIso_apply, BumpCovering.sum_toPartitionOfUnity_eq, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_invApp_assoc, Path.extend_one, ContinuousMap.exists_tendsto_compactOpen_iff_forall, ContinuousMap.sigmaCodHomeomorph_symm_apply, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.stalk_iso, ContinuousMap.coe_mk, ContinuousMap.coeFn_toLp, PartitionOfUnity.sum_le_one, NonUnitalContinuousFunctionalCalculus.exists_cfc_of_predicate, Circle.exp_int_mul_two_pi, ContinuousMap.congr_fun, TopCat.GlueData.image_inter, curveIntegral_eq_intervalIntegral_deriv, ContinuousMap.equivFnOfDiscrete_symm_apply_apply, ContinuousMap.Homotopy.affine_apply, StarAlgHom.realContinuousMapOfNNReal_injective, TopCat.isEmbedding_pullback_to_prod, ContinuousMap.isUniformEmbedding_uniformFunOfFun, ContinuousMap.linearIsometryBoundedOfCompact_toAddEquiv, ContinuousMap.instSecondCountableTopology, BoundedContinuousFunction.compContinuous_apply, ContinuousMap.nnnorm_eq_iSup_nnnorm, AlgebraicGeometry.Flat.stalkMap, fourier_neg, cfcHom_isStrictlyPositive_iff, AlgebraicGeometry.Scheme.Pullback.range_snd, AlgebraicGeometry.Scheme.Opens.germ_stalkIso_hom_assoc, AlgebraicGeometry.Scheme.Hom.stalkMap_comp, ContinuousMap.zsmul_comp, AlexDisc.forgetToTop_full, TopCat.pullbackIsoProdSubtype_hom_apply, ContinuousMap.toLp_comp_toContinuousMap, AlgebraicGeometry.Scheme.Cover.exists_eq, HomotopyGroup.inv_spec, AlgebraicGeometry.Scheme.ofArrows_mem_precoverage_iff, BoundedContinuousFunction.toContinuousMapStarₐ_apply_apply, Path.range_coe, ContinuousMap.nndist_eq_iSup, AlgebraicGeometry.Scheme.IsLocallyDirected.ι_jointly_surjective, AlgebraicGeometry.IsPreimmersion.base_embedding, AlgebraicGeometry.Scheme.Hom.coe_image, AlgebraicGeometry.Scheme.Hom.coe_preimage, ContinuousMap.equivFnOfDiscrete_symm_apply, ContinuousMap.norm_restrict_mono_set, ContinuousMap.exists_finite_sum_smul_approximation_of_mem_uniformity, TopCat.ofHom_apply, Homeomorph.compStarAlgEquiv'_apply, AlgebraicGeometry.LocallyRingedSpace.stalkSpecializes_stalkMap_apply, ContinuousMap.Homotopic.equivalence, AlgebraicGeometry.Spec.coe_toTop_map_hom_apply_asIdeal, TopCat.coneOfConeForget_π_app, LightDiagram.id_hom_hom_hom_apply, ContinuousMap.add_apply, cfc_apply_pi, ContinuousMap.one_comp, RingHom.compLeftContinuous_apply_apply, ContinuousMapZero.toContinuousMapHom_apply, ContinuousMap.coe_natCast, ContinuousMap.comp_attachBound_mem_closure, AlgebraicGeometry.Scheme.Hom.isClosedEmbedding, AlgebraicGeometry.Scheme.Hom.quasiFiniteAt_iff_isOpen_singleton_asFiber, ContinuousMap.isometryEquivBoundedOfCompact_toEquiv, ContinuousMap.instRegularSpace, UniformOnFun.edist_continuousRestrict, ContinuousAddMonoidHom.isEmbedding_toContinuousMap, ContinuousMap.Homotopy.coe_toContinuousMap, AlgebraicGeometry.Scheme.Hom.finite_preimage_singleton, ContinuousMap.continuousOn_mkD_restrict_of_uncurry, ContinuousMap.Homotopy.apply_zero, ContinuousMap.tendsto_compactOpen_iff_forall, Matrix.IsHermitian.cfcAux_id, TopCat.induced_of_isLimit, ContinuousMap.adjoin_id_eq_span_one_add, Path.extend_symm, AlgebraicGeometry.Scheme.inv_hom_apply, Topology.WithGeneratedByTopology.isOpen_iff, Real.tsum_eq_tsum_fourier_of_rpow_decay, Circle.surjOn_exp_neg_pi_pi, ContinuousMap.apply_le_norm, ContinuousMap.continuous_mkD_restrict_of_uncurry, PadicInt.fwdDiff_mahlerSeries, AlgebraicGeometry.isIso_SpecMap_stakMap_localization, AlgebraicGeometry.Scheme.residue_residueFieldMap_assoc, ContinuousMap.instIsOrderedMonoid, BoundedContinuousFunction.norm_mkOfCompact, AlgebraicGeometry.Scheme.IdealSheafData.support_map, CompactlySupportedContinuousMap.continuousMapEquiv_symm_apply, ContinuousMap.coe_star, BoundedContinuousFunction.mkOfCompact_one, AlgebraicGeometry.FormallyUnramified.stalkMap, Circle.exp_intCast_mul, TopCat.Presheaf.pushforwardPullbackAdjunction_unit_pullback_map_germToPullbackStalk, AlgebraicGeometry.PresheafedSpace.stalkMap.congr_hom, ContinuousMap.linearIsometryBoundedOfCompact_apply_apply, AddMonoidHom.compLeftContinuous_apply, ContinuousMap.sub_comp, TopCat.prodIsoProd_hom_apply, CompHausLike.toCompHausLike_map, cfcHomSuperset_id, ContinuousMap.hasFiniteIntegral_mkD_of_bound, AlgebraicGeometry.Scheme.OpenCover.finiteSubcover_X, ContinuousMap.coe_coe, AlgebraicGeometry.Scheme.Pullback.range_fst, BumpCovering.eventuallyEq_one', TopCat.comp_app, ContinuousMap.instLocallyConvexSpace, AlgebraicGeometry.IsOpenImmersion.iff_stalk_iso, AlexDisc.Iso.mk_hom, AlgebraicGeometry.Scheme.Cover.fromGlued_isOpenEmbedding, ContinuousMap.Homotopy.evalAt_affine, AlgebraicGeometry.Scheme.residue_residueFieldMap, ContinuousMap.coe_sum, exists_continuousMap_one_of_isCompact_subset_isOpen, ContinuousMonoidHom.isClosedEmbedding_toContinuousMap, ContinuousMonoidHom.range_toContinuousMap, AlgebraicGeometry.PresheafedSpace.stalkMap.comp, BoundedContinuousFunction.coe_toContinuousMapₐ, AlgHom.compLeftContinuous_apply_apply, ContinuousMap.HomotopyWith.prop, TopCat.pullbackIsoProdSubtype_inv_snd_assoc, ContinuousMap.restrict_apply_mk, TopCat.epi_iff_surjective, AlgebraicGeometry.Scheme.stalkMap_inv_hom_apply, TopologicalSpace.Opens.comap_injective, QuasispectrumRestricts.nnreal_of_nonneg, AlgebraicGeometry.Scheme.SpecMap_residue_apply, TopologicalSpace.Opens.coe_comap, ContinuousMap.equivBoundedOfCompact_symm_apply, ContinuousMap.instIsCentralScalar, ContinuousMap.HomotopyWith.refl_apply, ZeroAtInftyContinuousMap.coe_toContinuousMap, Real.fourierChar_apply', AlgebraicGeometry.Scheme.Pullback.range_diagonal_subset_diagonalCoverDiagonalRange, ContinuousMap.mkD_eq_self, FundamentalGroupoid.map_obj_as, TopCat.instIsRightAdjointForgetContinuousMapCarrier, AlgebraicGeometry.Scheme.Hom.mem_smoothLocus, PartitionOfUnity.le_one, TopCat.GlueData.fromOpenSubsetsGlue_isOpenMap, WeakDual.gelfandTransform_apply_apply, AlgebraicGeometry.IsAffineOpen.isoSpec_hom_apply, ContinuousMap.continuous_comp', Path.extend_zero, ContinuousMap.Homotopy.extend_zero, ContinuousMap.nsmul_apply, Homeomorph.coe_toHomotopyEquiv, BumpCovering.nonneg, ContinuousMapZero.isUniformEmbedding_toContinuousMap, Path.coe_toContinuousMap, bernsteinApproximation_uniform, ContinuousMap.Homotopy.map_one_left, AlgebraicGeometry.Scheme.Pullback.Triplet.Spec_ofPointTensor_SpecTensorTo, PadicInt.mahlerEquiv_apply, ContinuousMap.Homotopy.apply_one, ContinuousMap.compStarAlgHom_id, TopologicalSpace.Fiber.sigmaIsoHom_surj, TopCat.adj₂_counit, ContinuousMap.hasFiniteIntegral_mkD_restrict_of_bound, AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint_s, AlgebraicGeometry.QuasiCompactCover.isCompactOpenCovered_of_isAffineOpen, ContinuousMap.coe_div, AlgebraicGeometry.Scheme.Opens.range_ι, AlgebraicGeometry.IsAffineOpen.range_fromSpec, BumpCovering.exists_finset_toPOUFun_eventuallyEq, GenLoop.Homotopic.equiv, AlgebraicGeometry.isClosedImmersion_iff, ContinuousMap.injective_restrict, AlgebraicGeometry.LocallyRingedSpace.Γevaluation_naturality_assoc, ContinuousMap.tendsto_nhds_compactOpen, TopModuleCat.instPreservesLimitsTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrier, Path.truncate_const_continuous_family, AlgebraicGeometry.Spec_closedPoint, AlgebraicGeometry.Scheme.Hom.range_subset_ker_support, exists_continuous_one_zero_of_isCompact_of_isGδ, Profinite.NobelingProof.spanFunctorIsoIndexFunctor_inv_app, fourierSubalgebra_closure_eq_top, AlgebraicGeometry.ProjectiveSpectrum.Proj.stalkMap_toSpec, TopCat.hom_inv_id_apply, Filter.HasBasis.compactConvergenceUniformity_of_compact, TopCat.nonempty_isColimit_iff_eq_coinduced, AlgebraicGeometry.Scheme.Hom.finite_preimage, AlgebraicGeometry.Scheme.Opens.ι_apply, LightProfinite.surjective_transitionMap, CompHaus.epi_iff_surjective, TopCat.mono_iff_injective, ContinuousMap.natCast_apply, AlgebraicGeometry.Scheme.iso_inv_base_hom_base_apply, AlgebraicGeometry.Scheme.Hom.continuous, AlgebraicGeometry.Scheme.Hom.asFiberHom_fiberToSpecResidueField, BoundedContinuousFunction.toContinuousMapₐ_apply, TopCat.homeoOfIso_symm_apply, AlgebraicGeometry.Scheme.Pullback.Triplet.exists_preimage, AlgebraicGeometry.Scheme.Hom.isConstructible_image, AlgebraicGeometry.Scheme.Hom.stalkMap_hom_inv_apply, AlgebraicGeometry.Surjective.surj, ContinuousMap.coe_mabs, cfc_eq_cfcL, AlgebraicGeometry.Scheme.stalkMap_inv_hom, ContinuousMap.yonedaPresheaf'_map, ContinuousMap.mem_setOfIdeal, LightProfinite.epi_iff_surjective, ContinuousLinearMap.IsPositive.spectrumRestricts, AlgebraicGeometry.Scheme.comp_base_apply, AlgebraicGeometry.isGermInjectiveAt_iff_of_isOpenImmersion, ContinuousMap.fst_apply, TopCat.GlueData.MkCore.t_inter, AlgebraicGeometry.PresheafedSpace.GlueData.ι_jointly_surjective, PartitionOfUnity.sum_nonneg, AlgebraicGeometry.IsAffineOpen.isoSpec_hom_base_apply, polynomialFunctions.topologicalClosure, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_apply_eq_comap, Topology.IsGeneratedBy.isClosed_iff, ContinuousMap.concatCM_right, ContinuousMap.hasBasis_compactConvergenceUniformity_of_compact, Path.extend_extends', AlgebraicGeometry.IsDominant.denseRange, nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts, AlgebraicGeometry.Flat.iff_flat_stalkMap, ContinuousMap.coe_inv, AlgebraicGeometry.Scheme.preimage_zeroLocus, ContinuousMap.smul_apply', ContinuousMap.const_apply, AlgebraicGeometry.isIso_iff_stalk_iso, AlgebraicGeometry.Scheme.instIsOverMapStalkMapOverInferInstanceOverClass, cfcHom_predicate, WeakDual.CharacterSpace.continuousMapEval_apply_apply, NNReal.coeNNRealReal_zero, Path.truncate_continuous_family, TopCat.GlueData.ι_jointly_surjective, CompHausLike.isoOfHomeo_inv_hom_hom_apply, AlgebraicGeometry.Scheme.Hom.support_ker, AlgebraicGeometry.Scheme.Hom.homeomorph_apply, AlgebraicGeometry.Scheme.Hom.stalkMap_congr, ContinuousMap.addEquivBoundedOfCompact_symm_apply, UnitAddTorus.span_mFourier_closure_eq_top, ContinuousMap.homeoFnOfDiscrete_symm_apply_apply, ContinuousMap.IccExtendCM_of_mem, isLocalHomeomorph_circleExp, ContinuousMap.idealOfEmpty_eq_bot, PadicInt.norm_mahler_eq, ContinuousMap.C_apply, ContinuousMap.polynomial_comp_attachBound, CompHausLike.hom_ofHom, AlgebraicGeometry.Scheme.germ_stalkClosedPointTo_Spec, AlgebraicGeometry.LocallyRingedSpace.stalkSpecializes_stalkMap, norm_cfcHom, ContinuousMap.instContinuousConstSMul, ContinuousMap.continuous_precomp, AlgebraicGeometry.Scheme.Hom.surjective, ContinuousMap.isOpen_setOf_range_subset, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.sigma_ι_isOpenEmbedding, ContinuousMap.aeStronglyMeasurable_mkD_of_uncurry, AlgebraicGeometry.Scheme.IsLocallyDirected.exists_of_pullback_V_V, ContinuousMap.mabs_apply, AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.imageBasicOpen_image_preimage, ContinuousMap.evalAlgHom_apply, TopCat.isOpen_iff_of_isColimit_cofork, fourierCoeffOn_eq_integral, ContinuousMap.toNNReal_neg_one, Circle.expHom_apply, ContinuousMap.coe_prod, IsLocalHomeomorph.isTopologicalBasis, MonoidHom.compLeftContinuous_apply, Filter.HasBasis.nhds_continuousMapConst, LightDiagram.comp_hom_hom_hom_apply, TopModuleCat.instReflectsIsomorphismsTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrier, ContinuousMap.pi_eval, TopCat.isQuotientMap_of_isColimit_cofork, ContinuousMap.exists_disjoint_nonempty_clopen_cover_of_mem_nhds_diagonal, TopCat.forget_preservesColimitsOfSize, UnitAddTorus.mFourier_single, ContinuousMap.coe_mulLeft, AlgebraicGeometry.Scheme.Hom.stalkMap_congr_assoc, ContinuousMap.instContinuousAddOfLocallyCompactSpace, ContinuousMap.ker_evalStarAlgHom_inter_adjoin_id, Action.isContinuous_def, ContinuousOn.tendsto_restrict_iff_tendstoUniformlyOn, AlgebraicGeometry.Scheme.stalkMap_inv_hom_assoc, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.preimage_toBase_eq_range_ι, TopCat.isOpen_iff_of_isColimit, AlgebraicGeometry.locallyQuasiFinite_iff_finite_preimage_singleton, AlgebraicGeometry.Spec.topObj_forget, TopCat.adj₂_unit, Circle.arg_exp, cfcHomSuperset_continuous, ContinuousMap.isComplete_setOf_eqOn, SpectrumRestricts.nnreal_iff_spectralRadius_le, TopologicalSpace.OpenNhds.map_id_obj, PartitionOfUnity.finite_tsupport, integrable_mulExpNegMulSq_comp_restrict_of_isCompact, TopCat.forget_preservesLimits, AlgebraicGeometry.Scheme.Opens.ι_appLE, ContinuousMap.compRightAlgHom_continuous, Filter.Tendsto.pathExtend, MeasureTheory.Lp.compMeasurePreserving_continuous, AlgebraicGeometry.IsOpenImmersion.range_pullbackFst, AlgebraicGeometry.IsAffineOpen.fromSpec_image_zeroLocus, mahler_apply, AlgebraicGeometry.Scheme.affineBasisCover_map_range, MeasureTheory.FiniteMeasure.continuous_iff_forall_continuousMap_continuous_integral, ContinuousMap.isClosed_setOf_mapsTo, ContinuousMap.HomotopyRel.eq_fst, ContinuousMap.elemental_id_eq_top, AlgebraicGeometry.Flat.isQuotientMap_of_surjective, AlgebraicGeometry.Scheme.Opens.ι_app, AlgebraicGeometry.Scheme.Hom.QuasiFiniteAt.isClopen_singleton_asFiber, AlgebraicGeometry.instIsPreimmersionAsFiberHom, gelfandTransform_isometry, EMetric.exists_continuous_eNNReal_forall_closedBall_subset, AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr_hom_assoc, hasSum_one_div_pow_mul_fourier_mul_bernoulliFun, polynomialFunctions_closure_eq_top', ContinuousMap.instIsCountablyGeneratedProdUniformityOfWeaklyLocallyCompactSpaceOfSigmaCompactSpace, CompHausLike.LocallyConstant.incl_comap, AlgebraicGeometry.quasiCompact_iff_spectral, AlgebraicGeometry.Scheme.iso_hom_base_inv_base_apply, TopCat.prodIsoProd_inv_fst_apply, bernstein.probability, ContinuousMap.mem_idealOfSet_compl_singleton, AlgebraicGeometry.quasiCompact_iff_isSpectralMap, ContinuousMap.compStarAlgHom'_apply, ContinuousMap.norm_smul_const, ContinuousMap.add_comp, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_preimage_basicOpen, starContinuousMap_apply, ContinuousMap.pow_comp, TopCat.effectiveEpi_iff_isQuotientMap, ContinuousMap.compRightContinuousMap_apply, TopCat.colimit_isOpen_iff, Homeomorph.compStarAlgEquiv'_symm_apply, ContinuousMap.polynomial_comp_attachBound_mem, TopCat.adj₁_unit, range_cfcHom, Circle.coe_exp, ContinuousMap.unitsLift_symm_apply_apply_inv', ContinuousMap.coe_one, ContinuousMap.isometryEquivBoundedOfCompact_symm_apply, LightProfinite.proj_surjective, ContinuousMap.instSubsingletonOfIsEmpty, CStarAlgebra.nonneg_TFAE, nnnorm_cfcHom, AlgebraicGeometry.LocallyRingedSpace.toΓSpec_preimage_zeroLocus_eq, fourier_add', Circle.exp_zsmul, MeasureTheory.Integrable.fourier_smul, AlgebraicGeometry.IsAffineOpen.isCompactOpenCovered, ContinuousMap.nhds_compactOpen, ContinuousMap.HomotopyWith.apply_zero, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.base_open, TopCat.adj₁_counit, ContinuousMap.zero_comp, alexDiscEquivPreord_counitIso, PadicInt.mahlerEquiv_symm_apply, AlgebraicGeometry.Scheme.Γevaluation_naturality, Circle.exp_eq_one, TopCat.GlueData.ι_eq_iff_rel, UniformOnFun.edist_continuousRestrict_of_singleton, MeasureTheory.ProbabilityMeasure.continuous_iff_forall_continuousMap_continuous_lintegral, PartitionOfUnity.mem_fintsupport_iff, Polynomial.toAddCircle_X_eq_fourier_one, AlgebraicGeometry.HasRingHomProperty.stalkMap_of_respectsIso, ContinuousMap.Homotopy.refl_apply, ContinuousMap.HomotopyEquiv.continuous, AlgebraicGeometry.ExistsHomHomCompEqCompAux.range_g_subset, BumpCovering.toPOUFun_eq_mul_prod, TopologicalSpace.Opens.toTopCat_map, ContinuousMap.toNNReal_add_add_neg_add_neg_eq, ContinuousMap.eval_apply, fourier_add_half_inv_index, fourierCoeffOn_of_hasDerivAt, ContinuousMap.snd_apply, Path.extend_of_le_zero, integrable_mulExpNegMulSq_comp, AlgebraicGeometry.Scheme.isLocalHom_stalkClosedPointTo, ContinuousMap.compactOpen_le_induced, AlgebraicGeometry.LocallyRingedSpace.Γevaluation_naturality, CondensedSet.toTopCatMap_hom_apply, TopCat.Presheaf.germToPullbackStalk_stalkPullbackHom_assoc, Filter.HasBasis.compactConvergenceUniformity, exists_tsupport_one_of_isOpen_isClosed, ContinuousMap.ker_evalStarAlgHom_eq_closure_adjoin_id, abs_integral_sub_setIntegral_mulExpNegMulSq_comp_lt, SchwartzMap.tsum_eq_tsum_fourierIntegral, ContinuousMap.idealOf_compl_singleton_isMaximal, AlgebraicGeometry.Scheme.Hom.SpecMap_residueFieldMap_fromSpecResidueField, SmoothPartitionOfUnity.toPartitionOfUnity_toFun, TopCat.coe_comp, ContinuousMap.measurable, fourier_add, CompHausLike.isoOfHomeo_hom_hom_hom_apply, AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint_y, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_invApp_assoc, AlgebraicGeometry.LocallyRingedSpace.evaluation_naturality_assoc, AlgebraicGeometry.LocallyRingedSpace.toStalk_stalkMap_toΓSpec, AlgebraicGeometry.Scheme.range_fromSpecResidueField, ContinuousMap.exists_mem_subalgebra_near_continuous_of_separatesPoints, AlgebraicGeometry.Scheme.SpecMap_stalkMap_fromSpecStalk, BumpCovering.locallyFinite', TopCat.exists_mem_zeroHypercover_range, AlgebraicGeometry.PresheafedSpace.stalkMap.stalkSpecializes_stalkMap_assoc, ContinuousMap.Homotopy.extend_one, PartitionOfUnity.exists_finset_nhds', ContinuousMap.compStarAlgHom_apply, UniformFun.edist_continuousMapMk, TopCat.sigmaIsoSigma_hom_ι_apply, AlgebraicGeometry.Scheme.Hom.stalkMap_inv_hom_apply, ContinuousMap.instR0Space, IsometricContinuousFunctionalCalculus.isometric, ContinuousMap.intCast_apply, ContinuousMap.coe_smul, AlgebraicGeometry.quasiCompactCover_iff, AlgebraicGeometry.Scheme.image_zeroLocus, BumpCovering.le_one', PartitionOfUnity.exists_pos, ContinuousMap.Homotopy.curry_one, ContinuousMap.mul_comp, ContinuousMap.range_toUniformOnFunIsCompact, AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField_apply, AlgebraicGeometry.Scheme.Hom.stalkMap_hom_inv_assoc, Path.coe_mk', Path.truncate_one_one, ContinuousMap.coe_pow, MeasureTheory.ContinuousMap.inner_toLp, ContinuousMapZero.toContinuousMap_injective, CompactExhaustion.hasBasis_compactConvergenceUniformity, AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint_SpecTensorTo, ContinuousMap.enorm_eq_iSup_enorm, Circle.isCoveringMap_exp, ContinuousMap.compStarAlgHom'_id, AlgebraicGeometry.Scheme.JointlySurjective.exists_eq, AddChar.zmod_intCast, ContinuousMap.isometryEquivBoundedOfCompact_apply, LightCondSet.toTopCatMap_hom_apply, ContinuousMap.coe_const, AlgebraicGeometry.LocallyRingedSpace.isLocalHom_stalkMap_congr, TopCat.ext_iff, BoundedContinuousFunction.mkOfCompact_sub, ContinuousMap.uniform_continuity, AlgebraicGeometry.Scheme.Hom.app_appIso_inv, TopCat.limit_topology, Polynomial.toContinuousMapOn_apply, ContinuousMap.Homotopy.extend_apply_of_le_zero, ContinuousMap.HomotopyEquiv.trans_symm_apply, TopCat.Presheaf.stalkSpecializes_stalkPushforward_assoc, ContinuousMap.instR1Space, AlgebraicGeometry.Scheme.coe_homeoOfIso, Polynomial.toAddCircle_C_eq_smul_fourier_zero, TopCat.Presheaf.stalkPushforward.comp, AlgebraicGeometry.LocallyRingedSpace.stalkSpecializes_stalkMap_assoc, polynomialFunctions_closure_eq_top, BoundedContinuousFunction.separatesPoints_charPoly, ContinuousMap.coe_mul, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec.image_basicOpen_eq_basicOpen, AlgebraicGeometry.isClosedMap_iff_specializingMap, TopCat.pullback_snd_range, AlgebraicGeometry.Scheme.image_preimage_eq_of_isPullback, AlgebraicGeometry.Scheme.Hom.instIsLocalHomCarrierStalkCommRingCatPresheafCoeContinuousMapCarrierCarrierHomTopCatBaseRingHomHomStalkMap, ProfiniteGrp.instPreservesLimitsProfiniteForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, AlgebraicGeometry.LocallyRingedSpace.stalkMap_comp, AlgebraicGeometry.Scheme.GlueData.ι_jointly_surjective, AlgebraicGeometry.SheafedSpace.isColimit_exists_rep, ContinuousMap.continuous_curry, cfcHom_eq_of_isStarNormal, AlexDisc.forgetToTop_of, ContinuousMap.continuousAt, Real.tsum_eq_tsum_fourierIntegral_of_rpow_decay, Circle.exp_sub_two_pi, TopCat.GlueData.MkCore.cocycle, ContinuousMapZero.coe_toContinuousMapHom, AlgebraicGeometry.LocallyRingedSpace.stalkMap_hom_inv_apply, TopologicalSpace.OpenNhds.inclusionMapIso_inv_app, AlgebraicGeometry.Scheme.stalkClosedPointTo_comp, AlgebraicGeometry.LocallyRingedSpace.evaluation_naturality_apply, ContinuousMap.instT0Space, Circle.argPartialEquiv_symm_apply, AlgebraicGeometry.Scheme.Spec_map_residue_apply, ContinuousMap.zsmul_apply, BumpCovering.exists_isSubordinate_hasCompactSupport_of_locallyFinite_t2space, Polynomial.fourierCoeff_toAddCircle, TopCat.GlueData.ι_injective, Path.uniformContinuous_extend, cfcHom_map_spectrum, AlgebraicGeometry.Scheme.residueFieldMap_comp, ContinuousMap.isUnit_iff_forall_ne_zero, BoundedContinuousFunction.dist_mkOfCompact, AlgebraicGeometry.Scheme.isoSpec_image_zeroLocus, ContinuousMap.linearIsometryBoundedOfCompact_toIsometryEquiv, AlgebraicGeometry.Scheme.Hom.fiberι_fiberHomeo_symm, GenLoop.boundary, GenLoop.homotopyFrom_apply, GenLoop.const_apply, PartitionOfUnity.continuous_smul, AlgebraicGeometry.Scheme.Spec_stalkClosedPointTo_fromSpecStalk, ContinuousMap.id_apply, TopCat.Presheaf.pushforwardPullbackAdjunction_unit_pullback_map_germToPullbackStalk_assoc, LightProfinite.proj_comp_transitionMap', AlgebraicGeometry.LocallyRingedSpace.isLocalHomValStalkMap, ContinuousMap.const_zero, TopCat.coconeOfCoconeForget_ι_app, AlgebraicGeometry.Scheme.mem_toGrothendieck_smallPretopology, AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr_point, ContinuousCohomology.const_app_hom, PartitionOfUnity.sum_finsupport', AlgebraicGeometry.Scheme.Hom.stalkMap_inv_hom, ProfiniteGrp.instIsTopologicalGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousMonoidHomToProfiniteContinuousMap, ContinuousMap.mul_apply, ContinuousMap.dist_le_iff_of_nonempty, ContinuousMap.compRightAlgHom_apply, ContinuousMap.addUnitsLift_symm_apply_apply_neg', ContinuousMap.sub_apply, GenLoop.fromLoop_coe, AlgebraicGeometry.Scheme.Hom.Spec_map_residueFieldMap_fromSpecResidueField, AlgebraicGeometry.Scheme.Opens.toSpecΓ_preimage_zeroLocus, AlgebraicGeometry.Scheme.Cover.fromGlued_open_map, TopCat.inv_hom_id_apply, BumpCovering.sum_toPOUFun_eq, alexDiscEquivPreord_functor, GenLoop.homotopicTo, AlgebraicGeometry.coprodMk_inr, ContinuousMap.idealOfSet_ofIdeal_eq_closure, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_bijective, ContinuousAddMonoidHom.toContinuousMap_injective, continuousFunctionalCalculus_map_id, fourierCoeffOn_of_hasDeriv_right, AlgebraicGeometry.Scheme.Hom.isProperMap, ContinuousMap.continuous_mkD_of_uncurry, ContinuousMap.instNormOneClassOfNonempty, AlgebraicGeometry.QuasiCompactCover.exists_isAffineOpen_of_isCompact, ContinuousMap.toFun_eq_coe, AlgebraicGeometry.Scheme.Hom.asFiberHom_fiberToSpecResidueField_assoc, ContinuousMap.sup'_apply, BumpCovering.coe_single, ContinuousMap.instMetrizableSpace, GenLoop.continuous_toLoop, ContinuousMap.isUniformEmbedding_equivBoundedOfCompact, GenLoop.fromLoop_trans_toLoop, TopCat.pullback_fst_range, AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr_hom, TopologicalSpace.OpenNhds.inclusionMapIso_hom_app, Path.extend_trans_of_half_le, AlgebraicGeometry.Scheme.Hom.isOpen_smoothLocus, ContinuousMap.idealOfSet_isMaximal_iff, AlgebraicGeometry.Scheme.stalkSpecializes_stalkMap_assoc, AlgebraicGeometry.Scheme.Opens.ι_base_apply, SpectrumRestricts.nnreal_iff_nnnorm, ZMod.toCircle_eq_circleExp, Polynomial.toContinuousMapOnAlgHom_apply, TopCat.Presheaf.stalkSpecializes_stalkPushforward_apply, curveIntegralFun_def, AlgebraicGeometry.Scheme.Hom.isDiscrete_preimage, Circle.exp_nsmul, coeFn_fourierLp, Path.truncate_range, BoundedContinuousFunction.coe_toContinuousMap, TopCat.GlueData.preimage_image_eq_image', ContinuousMap.Homotopy.map_zero_left, AlgebraicGeometry.Scheme.homOfLE_apply, cfcHom_apply_mem_elemental, LocallyConstant.coe_continuousMap, AlgebraicGeometry.IsAffineOpen.fromSpec_primeIdealOf, TopCat.pullback_snd_image_fst_preimage, ContinuousMap.instSeparableSpace, Stonean.effectiveEpi_tfae, ContinuousMap.coe_IccExtend, ContinuousMap.edist_eq_iSup, Topology.WithGeneratedByTopology.isClosed_iff, AlgebraicGeometry.LocallyRingedSpace.iso_hom_base_inv_base_apply, Topology.IsGeneratedBy.continuous_iff, CompHausLike.coe_comp, LightProfinite.isClosedEmbedding_natUnionInftyEmbedding, CompHausLike.finiteCoproduct.ι_jointly_surjective, AlgebraicGeometry.Scheme.fromSpecResidueField_apply, ContinuousMap.const_one, ContinuousMapZero.isClosedEmbedding_toContinuousMap, LocallyConstant.toContinuousMapAlgHom_apply, TopModuleCat.hom_forget₂_TopCat_map, AlgebraicGeometry.Scheme.Hom.coe_opensRange, ContinuousMap.instSMulCommClass, AlgebraicGeometry.Scheme.stalkMap_congr, Path.eqOn_extend_segment, PartitionOfUnity.sum_finsupport, ContinuousMap.instIsScalarTower_1, AlgebraicGeometry.Scheme.Hom.stalkMap_congr_hom, BoundedContinuousFunction.coe_compContinuous, RCLike.restrict_toContinuousMap_eq_toContinuousMapStar_restrict, ContinuousMap.isClopen_setOf_mapsTo, ContinuousMap.coeFnMonoidHom_apply, ContinuousMap.instTrivialStar, ContinuousMap.HomotopyEquiv.refl_apply, GenLoop.instContinuousEvalConst, AlgebraicGeometry.SheafedSpace.GlueData.ι_jointly_surjective, DeltaGeneratedSpace.continuous_iff, ContinuousMap.dist_eq_iSup, ContinuousMap.coe_abs, AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_apply, AlgebraicGeometry.PresheafedSpace.stalkMap.congr_point, ContinuousMap.exists_extension', contMDiff_circleExp, SchwartzMap.tsum_eq_tsum_fourier, ContinuousMapZero.range_toContinuousMap, ContinuousMap.prod_eval, ContinuousMap.coe_sup, ContinuousMap.HomotopyRel.eq_snd, bernsteinApproximation.apply, isometry_cfcHom, ContinuousMap.Homotopy.curry_zero, TopCat.prodIsoProd_inv_snd_apply, AlgebraicGeometry.Scheme.Spec_stalkClosedPointTo_fromSpecStalk_assoc, BumpCovering.support_toPartitionOfUnity_subset, DiscreteQuotient.map_proj, ContinuousMap.Homotopy.eq_diag_path, polynomialFunctions.comap_compRightAlgHom_iccHomeoI, ContinuousMap.neg_apply, Polynomial.fourierCoeff_toAddCircle_eq_zero_of_lt_zero, AlgebraicGeometry.Scheme.Cover.fromGlued_injective, AlgebraicGeometry.Spec.map_base_apply, ContinuousMap.instCanLiftForallCoeContinuous, PartitionOfUnity.mem_finsupport, AlgebraicGeometry.Scheme.Hom.stalkMap_surjective, CompactlySupportedContinuousMap.continuousMapEquiv_apply_toFun, ContinuousMap.exists_mul_le_one_eqOn_ge, ContinuousMap.mkD_apply_of_continuous, CompHausLike.finiteCoproduct.ι_desc_apply, fourierCoeff_fourier, IsCoveringMap.liftPath_trans, ContinuousMap.restrict_apply, LocallyConstant.comapₐ_apply_apply, AlgebraicGeometry.Scheme.toSpecΓ_base
|