| Name | Category | Theorems |
|---|
coev π | CompOp | 3 mathmath: coev_apply, continuous_coev, image_coev
|
compRightContinuousMap π | CompOp | 1 mathmath: compRightContinuousMap_apply
|
compactOpen π | CompOp | 202 mathmath: dense_setOf_contDiff, toLp_inj, instContinuousVAdd, instContinuousEvalOfLocallyCompactPair, compactOpen_eq_iInf_induced, Matrix.IsHermitian.isClosedEmbedding_cfcAux, instIsTopologicalGroup, Real.fourierCoeff_tsum_comp_add, ContinuousMapZero.isEmbedding_toContinuousMap, abs_mem_subalgebra_closure, hasBasis_nhds, ArzelaAscoli.isCompact_of_equicontinuous, Homotopy.extend_apply_of_one_le, span_fourier_closure_eq_top, continuous_prodMk_const, GenLoop.fromLoop_apply, toEquiv_homeoFnOfDiscrete, toLp_denseRange, ContinuousMonoidHom.isInducing_toContinuousMap, range_toLp, isOpen_setOf_mapsTo, specializes_coe, continuousMap_mem_subalgebra_closure_of_separatesPoints, UnitAddTorus.mFourierSubalgebra_closure_eq_top, summable_of_locally_summable_norm, cfcHom_continuous, polynomialFunctions.starClosure_topologicalClosure, instContinuousMulOfLocallyCompactSpace, cfcL_apply, toLp_norm_le, GenLoop.homotopyTo_apply, mem_nhds_iff, concatCM_left, continuous_postcomp, cfcHom_isClosedEmbedding, continuous_iff_continuous_uniformOnFun, continuous_compactOpen, GenLoop.loopHomeo_apply, UnitAddTorus.mFourierCoeff_toLp, coe_homeoFnOfDiscrete, ContinuousCohomology.I_obj_Ο_apply, isInducing_postcomp, continuous_toNNReal, Homotopy.pathExtend_evalAt, Homeomorph.continuousMapOfUnique_apply, ContinuousLinearMap.const_apply_apply, WeakDual.CharacterSpace.continuousMapEval_bijective, continuous_of_continuous_uncurry, continuousMap_mem_polynomialFunctions_closure, idealOfSet_closed, tendsto_of_antitone_of_pointwise, instT1Space, instPseudoMetrizableSpace, GenLoop.instContinuousEval, instIsTopologicalAddGroup, WeakDual.CharacterSpace.homeoEval_naturality, coe_const', Path.Homotopy.eval_apply, homeoFnOfDiscrete_symm_apply, inseparable_coe, compactOpen_eq, NormedSpace.exp_continuousMap_eq, continuousOn_mkD_of_uncurry, isEmbedding_sigmaMk_comp, aeStronglyMeasurable_restrict_mkD_restrict_of_uncurry, uncurry_apply, ContinuousFunctionalCalculus.exists_cfc_of_predicate, periodic_tsum_comp_add_zsmul, evalCLM_apply, Homotopy.extend_apply_coe, toLp_def, GenLoop.continuous_fromLoop, tendsto_of_monotone_of_pointwise, ContinuousMapZero.toContinuousMapCLM_apply, GenLoop.toLoop_apply, nhds_compactOpen_eq_iInf_nhds_induced, toLp_norm_eq_toLp_norm_coe, GenLoop.fromLoop_symm_toLoop, sup_mem_subalgebra_closure, fourierCoeff_toLp, ContinuousAddMonoidHom.isClosedEmbedding_toContinuousMap, homeoFnOfDiscrete_apply, Homeomorph.continuousMapOfUnique_symm_apply, instContinuousConstVAdd, inf_mem_subalgebra_closure, continuous_const', ContinuousLinearMap.compLeftContinuous_apply, continuousOn_of_continuousOn_uncurry, continuous_iff_continuous_uniformFun, sublattice_closure_eq_top, tendsto_iff_tendstoUniformly, ContinuousCohomology.I_map_hom, Trivialization.clift_self, instIsTopologicalSemiringOfLocallyCompactSpace, ContinuousAddMonoidHom.isInducing_toContinuousMap, cfc_eq_cfcL_mkD, instT3Space, HomotopyWith.extendProp, aeStronglyMeasurable_mkD_restrict_of_uncurry, Homotopy.curry_apply, tendsto_iff_forall_isCompact_tendstoUniformlyOn, continuous_coev, Trivialization.proj_clift, instContinuousSMul, continuous_restrict, Homotopy.extend_apply_of_mem_I, GenLoop.toLoop_apply_coe, continuous_uncurry, curry_apply, PadicInt.hasSum_mahlerSeries, ContinuousOn.continuous_restrict_iff_continuous_uniformOnFun, GenLoop.loopHomeo_symm_apply, subalgebra_topologicalClosure_eq_top_of_separatesPoints, aeStronglyMeasurable_restrict_mkD_of_uncurry, toLp_injective, UnitAddTorus.hasSum_mFourier_series_of_summable, PadicInt.hasSum_mahler, isHomeomorph_coe, coe_toLp, instT2Space, eventually_mapsTo, instContinuousEvalConst, continuous_uncurry_of_continuous, Homotopy.extend_of_mem_I, instIsTopologicalRingOfLocallyCompactSpace, ContinuousMonoidHom.isEmbedding_toContinuousMap, tendsto_iff_tendstoLocallyUniformly, exists_tendsto_compactOpen_iff_forall, sigmaCodHomeomorph_symm_apply, coeFn_toLp, instSecondCountableTopology, toLp_comp_toContinuousMap, comp_attachBound_mem_closure, instRegularSpace, ContinuousAddMonoidHom.isEmbedding_toContinuousMap, secondCountableTopology, continuousOn_mkD_restrict_of_uncurry, tendsto_compactOpen_iff_forall, continuous_mkD_restrict_of_uncurry, hasSum_fourier_series_of_summable, instLocallyConvexSpace, ContinuousMonoidHom.isClosedEmbedding_toContinuousMap, HomotopyWith.prop, continuous_comp', Homotopy.extend_zero, isEmbedding_postcomp, bernsteinApproximation_uniform, tendsto_of_tendstoLocallyUniformly, tendsto_nhds_compactOpen, fourierSubalgebra_closure_eq_top, ContinuousCohomology.I_obj_V_topologicalSpace, cfc_eq_cfcL, polynomialFunctions.topologicalClosure, concatCM_right, WeakDual.CharacterSpace.continuousMapEval_apply_apply, UnitAddTorus.span_mFourier_closure_eq_top, homeoFnOfDiscrete_symm_apply_apply, IccExtendCM_of_mem, instContinuousConstSMul, continuous_precomp, isOpen_setOf_range_subset, aeStronglyMeasurable_mkD_of_uncurry, Filter.HasBasis.nhds_continuousMapConst, instContinuousAddOfLocallyCompactSpace, ContinuousOn.tendsto_restrict_iff_tendstoUniformlyOn, cfcHomSuperset_continuous, compRightAlgHom_continuous, MeasureTheory.Lp.compMeasurePreserving_continuous, isClosed_setOf_mapsTo, elemental_id_eq_top, polynomialFunctions_closure_eq_top', compRightContinuousMap_apply, eventually_range_subset, nhds_compactOpen, compactOpen_le_induced, ker_evalStarAlgHom_eq_closure_adjoin_id, Homotopy.extend_one, starSubalgebra_topologicalClosure_eq_top_of_separatesPoints, instR0Space, Homotopy.curry_one, MeasureTheory.ContinuousMap.inner_toLp, Homotopy.extend_apply_of_le_zero, instR1Space, polynomialFunctions_closure_eq_top, continuous_curry, instT0Space, GenLoop.homotopyFrom_apply, ContinuousCohomology.const_app_hom, GenLoop.fromLoop_coe, GenLoop.homotopicTo, idealOfSet_ofIdeal_eq_closure, continuous_mkD_of_uncurry, instMetrizableSpace, GenLoop.continuous_toLoop, GenLoop.fromLoop_trans_toLoop, compactOpen_eq_generateFrom, instSeparableSpace, idealOpensGI_choice, ContinuousMapZero.isClosedEmbedding_toContinuousMap, isClopen_setOf_mapsTo, GenLoop.instContinuousEvalConst, Homotopy.curry_zero
|
const' π | CompOp | 1 mathmath: coe_const'
|
curry π | CompOp | 3 mathmath: GenLoop.toLoop_apply_coe, curry_apply, continuous_curry
|
homeoFnOfDiscrete π | CompOp | 5 mathmath: toEquiv_homeoFnOfDiscrete, coe_homeoFnOfDiscrete, homeoFnOfDiscrete_symm_apply, homeoFnOfDiscrete_apply, homeoFnOfDiscrete_symm_apply_apply
|
uncurry π | CompOp | 3 mathmath: uncurry_apply, continuous_uncurry, GenLoop.fromLoop_coe
|