| Name | Category | Theorems |
|---|
comp 📖 | CompOp | 112 mathmath: FundamentalGroupoid.map_comp, compMonoidHom'_apply, exists_lift_sigma, comp_id, nsmul_comp, vadd_comp, ContinuousAt.compCM, Homotopic.comp, div_comp, Topology.WithLowerSet.map_comp, DiscreteQuotient.LEComap.comp, HomotopicRel.comp_continuousMap, TopologicalSpace.Opens.comap_comap, continuous_postcomp, piEquiv_symm_apply, comp_const, HomotopyEquiv.right_inv, Homeomorph.continuousMapCongr_symm_apply, ContinuousCohomology.I_obj_ρ_apply, uniformContinuous_comp_left, Homeomorph.continuousMapCongr_apply, isInducing_postcomp, TopCat.ofHom_comp, SpectralMap.coe_comp_continuousMap', topCatToSheafCompHausLike_map_val_app, Topology.IsQuotientMap.liftEquiv_symm_apply_coe, Homotopy.compContinuousMap_apply, Homotopy.comp_apply, coe_comp, WeakDual.CharacterSpace.homeoEval_naturality, HomotopyRel.compContinuousMap_apply, isEmbedding_sigmaMk_comp, neg_comp, CompactlySupportedContinuousMap.toContinuousMap_compLeft, compStarAlgHom'_comp, periodic_tsum_comp_add_zsmul, yonedaPresheaf_map, inv_comp, sigmaEquiv_symm_apply, StarAlgHom.realContinuousMapOfNNReal_apply_comp_toReal, cfcHom_comp, HomotopyEquiv.left_inv, comp_apply, CompHausLike.ofHom_comp, smul_comp, NNReal.ContinuousMap.canLift, uniformContinuous_comp, DiscreteQuotient.comap_comp, cancel_right, Filter.Tendsto.compCM, compAddMonoidHom'_apply, TopologicalSpace.Opens.comap_comp, exists_extension_forall_mem, cfcHomSuperset_apply, IsCoveringMap.homotopicRel_iff_comp, GenLoop.toLoop_apply_coe, id_comp, comp_one, concat_comp_IccInclusionLeft, comp_zero, zpow_comp, LocallyConstant.comap_comap, isUniformEmbedding_comp, const_comp, SpectrumRestricts.starAlgHom_apply, Nullhomotopic.comp_left, concat_comp_IccInclusionRight, Continuous.compCM, Homeomorph.toContinuousMap_comp_symm, IsCoveringMap.liftHomotopy_apply, ContinuousOn.compCM, sigmaCodHomeomorph_symm_apply, LocallyConstant.comap_comp, zsmul_comp, one_comp, comp_attachBound_mem_closure, Topology.IsQuotientMap.lift_comp, cancel_left, AddMonoidHom.compLeftContinuous_apply, sub_comp, continuous_comp', TopCat.toSheafCompHausLike_val_map, isEmbedding_postcomp, ContinuousWithinAt.compCM, exists_extension, yonedaPresheaf'_map, Homeomorph.coe_trans, Topology.WithUpperSet.map_comp, polynomial_comp_attachBound, continuous_precomp, isUniformInducing_comp, MonoidHom.compLeftContinuous_apply, comp_assoc, WeakDual.CharacterSpace.compContinuousMap_comp, compStarAlgHom'_apply, add_comp, pow_comp, compRightContinuousMap_apply, polynomial_comp_attachBound_mem, zero_comp, compStarAlgHom_apply, uniformSpace_eq_iInf_precomp_of_cover, Specialization.map_comp, mul_comp, Nullhomotopic.comp_right, Homeomorph.symm_comp_toContinuousMap, DiscreteQuotient.map_comp, TopCat.hom_comp, compRightAlgHom_apply, GenLoop.fromLoop_coe, isBigO_norm_restrict_cocompact, uniformSpace_eq_inf_precomp_of_cover
|
const 📖 | CompOp | 21 mathmath: continuous_prodMk_const, comp_const, Path.toHomotopyConst_apply, coe_const', IsCoveringMap.liftPath_const, nnnorm_smul_const, nullhomotopic_of_constant, continuous_const', comp_one, comp_zero, skyscraperPresheaf_eq_pushforward, const_comp, IsCoveringMap.liftHomotopy_apply, homotopic_const_iff, const_apply, Filter.HasBasis.nhds_continuousMapConst, norm_smul_const, coe_const, const_zero, Path.refl_extend, const_one
|
constPi 📖 | CompOp | 1 mathmath: constPi_apply
|
equivFnOfDiscrete 📖 | CompOp | 5 mathmath: toEquiv_homeoFnOfDiscrete, equivFnOfDiscrete_apply, coe_equivFnOfDiscrete, equivFnOfDiscrete_symm_apply_apply, equivFnOfDiscrete_symm_apply
|
eval 📖 | CompOp | 2 mathmath: piEquiv_symm_apply, eval_apply
|
fst 📖 | CompOp | 1 mathmath: fst_apply
|
id 📖 | CompOp | 42 mathmath: DiscreteQuotient.map_id, comp_id, ContinuousMapZero.toContinuousMap_id, Polynomial.toContinuousMapOn_X_eq_restrict_id, HomotopyEquiv.right_inv, cfcHom_id, Polynomial.toContinuousMap_X_eq_id, ContinuousFunctionalCalculus.exists_cfc_of_predicate, contractible_iff_id_nullhomotopic, TopCat.hom_id, CompHausLike.ofHom_id, DiscreteQuotient.leComap_id, HomotopyEquiv.left_inv, adjoin_id_eq_span_one_union, DiscreteQuotient.leComap_id_iff, Homeomorph.coe_refl, id_comp, coe_id, id_nullhomotopic, nonUnitalStarAlgebraAdjoin_id_subset_ker_evalStarAlgHom, Homeomorph.toContinuousMap_comp_symm, IsCoveringMap.liftHomotopy_apply, FundamentalGroupoid.map_id, NonUnitalContinuousFunctionalCalculus.exists_cfc_of_predicate, Topology.WithLowerSet.map_id, Matrix.IsHermitian.cfcAux_id, adjoin_id_eq_span_one_add, cfcHomSuperset_id, Specialization.map_id, ker_evalStarAlgHom_inter_adjoin_id, elemental_id_eq_top, TopologicalSpace.Opens.comap_id, ker_evalStarAlgHom_eq_closure_adjoin_id, LocallyConstant.comap_id, compStarAlgHom'_id, WeakDual.CharacterSpace.compContinuousMap_id, Homeomorph.symm_comp_toContinuousMap, id_apply, continuousFunctionalCalculus_map_id, TopCat.ofHom_id, DiscreteQuotient.comap_id, Topology.WithUpperSet.map_id
|
inclusion 📖 | CompOp | — |
instInhabited 📖 | CompOp | — |
liftCover 📖 | CompOp | 2 mathmath: liftCover_coe, liftCover_restrict
|
liftCover' 📖 | CompOp | 2 mathmath: liftCover_restrict', liftCover_coe'
|
mkD 📖 | CompOp | 20 mathmath: cfc_apply_mkD, mkD_of_continuousOn, mkD_of_not_continuousOn, continuousOn_mkD_of_uncurry, aeStronglyMeasurable_restrict_mkD_restrict_of_uncurry, mkD_of_not_continuous, cfc_eq_cfcL_mkD, aeStronglyMeasurable_mkD_restrict_of_uncurry, aeStronglyMeasurable_restrict_mkD_of_uncurry, mkD_apply_of_continuousOn, continuousOn_mkD_restrict_of_uncurry, continuous_mkD_restrict_of_uncurry, hasFiniteIntegral_mkD_of_bound, mkD_eq_self, hasFiniteIntegral_mkD_restrict_of_bound, ContinuousMapZero.mkD_eq_mkD_of_map_zero, aeStronglyMeasurable_mkD_of_uncurry, mkD_of_continuous, continuous_mkD_of_uncurry, mkD_apply_of_continuous
|
pi 📖 | CompOp | 4 mathmath: Homotopic.pi, piEquiv_apply, pi_eval, HomotopyRel.pi_apply
|
piEquiv 📖 | CompOp | 2 mathmath: piEquiv_symm_apply, piEquiv_apply
|
piMap 📖 | CompOp | 2 mathmath: piMap_apply, Homotopic.piMap
|
precomp 📖 | CompOp | — |
prodMap 📖 | CompOp | 2 mathmath: prodMap_apply, Homotopic.prodMap
|
prodMk 📖 | CompOp | 6 mathmath: HomotopyRel.prod_apply, continuous_prodMk_const, IsCoveringMap.liftHomotopy_apply, Homotopy.prod_apply, Homotopic.prodMk, prod_eval
|
prodSwap 📖 | CompOp | 1 mathmath: prodSwap_apply
|
restrict 📖 | CompOp | 35 mathmath: tendsto_compactOpen_restrict, compactOpen_eq_iInf_induced, ContinuousMapZero.toContinuousMap_id, TietzeExtension.exists_restrict_eq', Polynomial.toContinuousMapOn_X_eq_restrict_id, isBigO_norm_Icc_restrict_atTop, cfcHom_id, coe_restrict, ContinuousFunctionalCalculus.exists_cfc_of_predicate, adjoin_id_eq_span_one_union, nhds_compactOpen_eq_iInf_nhds_induced, exists_forall_mem_restrict_eq, liftCover_restrict', continuous_restrict, liftCover_restrict, nonUnitalStarAlgebraAdjoin_id_subset_ker_evalStarAlgHom, exists_tendsto_compactOpen_iff_forall, NonUnitalContinuousFunctionalCalculus.exists_cfc_of_predicate, norm_restrict_mono_set, exists_restrict_eq, tendsto_compactOpen_iff_forall, Matrix.IsHermitian.cfcAux_id, adjoin_id_eq_span_one_add, cfcHomSuperset_id, restrict_apply_mk, isBigO_norm_Icc_restrict_atBot, injective_restrict, exists_restrict_eq_forall_mem_of_closed, ker_evalStarAlgHom_inter_adjoin_id, elemental_id_eq_top, compactOpen_le_induced, ker_evalStarAlgHom_eq_closure_adjoin_id, continuousFunctionalCalculus_map_id, isBigO_norm_restrict_cocompact, restrict_apply
|
restrictPreimage 📖 | CompOp | 1 mathmath: restrictPreimage_apply
|
sigma 📖 | CompOp | 2 mathmath: sigma_apply, sigmaEquiv_apply
|
sigmaEquiv 📖 | CompOp | 3 mathmath: sigmaEquiv_symm_apply, sigmaEquiv_apply, piComparison_fac
|
sigmaMk 📖 | CompOp | 5 mathmath: exists_lift_sigma, isEmbedding_sigmaMk_comp, sigmaEquiv_symm_apply, sigmaMk_apply, sigmaCodHomeomorph_symm_apply
|
snd 📖 | CompOp | 1 mathmath: snd_apply
|