LocallyConstant

📁 Source: Mathlib/Topology/ContinuousMap/LocallyConstant.lean

Statistics

Metric	Count
Definitions LocallyConstant, toContinuousMapAddMonoidHom, toContinuousMapAlgHom, toContinuousMapLinearMap, toContinuousMapMonoidHom	5
Theorems toContinuousMapAddMonoidHom_apply, toContinuousMapAlgHom_apply, toContinuousMapLinearMap_apply, toContinuousMapMonoidHom_apply	4
Total	9

LocallyConstant

Definitions

Name	Category	Theorems
toContinuousMapAddMonoidHom 📖	CompOp	1 math math: toContinuousMapAddMonoidHom_apply
toContinuousMapAlgHom 📖	CompOp	1 math math: toContinuousMapAlgHom_apply
toContinuousMapLinearMap 📖	CompOp	1 math math: toContinuousMapLinearMap_apply
toContinuousMapMonoidHom 📖	CompOp	1 math math: toContinuousMapMonoidHom_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toContinuousMapAddMonoidHom_apply 📖	mathematical	—	DFunLike.coe AddMonoidHom LocallyConstant ContinuousMap AddZeroClass.toAddZero instAddZeroClass AddMonoid.toAddZeroClass ContinuousMap.instAddZeroClassOfContinuousAdd AddMonoidHom.instFunLike toContinuousMapAddMonoidHom toContinuousMap	—	—
toContinuousMapAlgHom_apply 📖	mathematical	—	DFunLike.coe AlgHom LocallyConstant ContinuousMap instSemiring ContinuousMap.instSemiringOfIsTopologicalSemiring instAlgebra ContinuousMap.algebra AlgHom.funLike toContinuousMapAlgHom toContinuousMap	—	—
toContinuousMapLinearMap_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LocallyConstant ContinuousMap instAddCommMonoid ContinuousMap.instAddCommMonoidOfContinuousAdd instModule ContinuousMap.module LinearMap.instFunLike toContinuousMapLinearMap toContinuousMap	—	—
toContinuousMapMonoidHom_apply 📖	mathematical	—	DFunLike.coe MonoidHom LocallyConstant ContinuousMap MulOneClass.toMulOne instMulOneClass Monoid.toMulOneClass ContinuousMap.instMulOneClassOfContinuousMul MonoidHom.instFunLike toContinuousMapMonoidHom toContinuousMap	—	—

(root)

Definitions

Name	Category	Theorems
LocallyConstant 📖	CompData	173 math math: LocallyConstant.congrRight_apply, LocallyConstant.apply_eq_of_isPreconnected, Profinite.NobelingProof.injective_πs', LocallyConstant.comapMonoidHom_apply, Profinite.NobelingProof.Products.span_nil_eq_top, LocallyConstant.congrLeftRingEquiv_apply_apply, LocallyConstant.coe_smul, LocallyConstant.charFn_eq_one, Profinite.NobelingProof.GoodProducts.linearIndependent_iff_union_smaller, Profinite.NobelingProof.coe_πs, LocallyConstant.range_finite, LocallyConstant.coe_comap_apply, Profinite.NobelingProof.instSubsingletonLocallyConstantElemForallBoolEmptyCollectionSetInt, Profinite.NobelingProof.instIsAddTorsionFreeLocallyConstantInt, LocallyConstant.congrRightₗ_symm_apply_apply, LocallyConstant.toContinuousMapLinearMap_apply, Profinite.NobelingProof.Products.max_eq_eval, Profinite.NobelingProof.Products.eval_πs, LocallyConstant.zero_apply, Profinite.NobelingProof.GoodProducts.injective, LocallyConstant.freeOfProfinite, LocallyConstant.comapRingHom_apply_apply, LocallyConstant.eval_apply, LocallyConstant.coe_zero, LocallyConstant.evalRingHom_apply, Profinite.NobelingProof.GoodProducts.equiv_toFun_eq_eval, LocallyConstant.evalMonoidHom_apply, LocallyConstant.coe_sub, Profinite.NobelingProof.Products.eval_πs', Profinite.NobelingProof.GoodProducts.span_sum, Profinite.NobelingProof.GoodProducts.range_equiv_factorization, LocallyConstant.continuous, LocallyConstant.congrRightₐ_apply_apply, CompHausLike.LocallyConstant.locallyConstantIsoContinuousMap_inv_apply, Profinite.NobelingProof.GoodProducts.spanFin, Profinite.NobelingProof.succ_exact, CompHausLike.LocallyConstantModule.functorToPresheaves_map_app, LocallyConstant.ext_iff, Profinite.NobelingProof.GoodProducts.smaller_factorization, LocallyConstant.congrRightₐ_symm_apply_apply, Profinite.NobelingProof.πs'_apply_apply, LocallyConstant.congrRightₗ_apply_apply, LocallyConstant.map_apply, LocallyConstant.congrLeftₐ_apply_apply, LocallyConstant.coeFnMonoidHom_apply, LocallyConstant.coeFnAddMonoidHom_apply, LocallyConstant.indicator_of_notMem, Profinite.NobelingProof.Products.eval_eq, LocallyConstant.indicator_apply, LocallyConstant.constAddMonoidHom_apply, Profinite.NobelingProof.Products.evalFacProps, LocallyConstant.ofIsClopen_fiber_zero, LocallyConstant.mapₐ_apply_apply, LocallyConstant.mulIndicator_apply, LocallyConstant.coe_comap, LocallyConstant.one_apply, LocallyConstant.congr_arg, LocallyConstant.evalₗ_apply, LocallyConstant.constₐ_apply_apply, LocallyConstant.comapAddMonoidHom_apply, Profinite.NobelingProof.instNontrivialLocallyConstantIntOfNonempty, LocallyConstant.toContinuousMap_injective, LocallyConstant.add_apply, LocallyConstant.toContinuousMapMonoidHom_apply, CompHausLike.LocallyConstant.functorToPresheaves_map_app, LocallyConstant.charFn_eq_zero, Profinite.NobelingProof.Products.eval_πs_image', Profinite.NobelingProof.factors_prod_eq_basis_of_ne, LocallyConstant.coeFnAlgHom_apply, LocallyConstant.toContinuousMapAddMonoidHom_apply, LocallyConstant.coe_mul, LocallyConstant.mapMonoidHom_apply, LocallyConstant.congrLeftRingEquiv_symm_apply_apply, Profinite.NobelingProof.GoodProducts.span, CompHausLike.LocallyConstant.locallyConstantIsoContinuousMap_hom, LocallyConstant.mapRingHom_apply_apply, Profinite.NobelingProof.GoodProducts.linearIndependent_iff_smaller, LocallyConstant.constRingHom_apply, LocallyConstant.evalAddMonoidHom_apply, LocallyConstant.apply_eq_of_preconnectedSpace, LocallyConstant.comapₗ_apply_apply, CompHausLike.LocallyConstantModule.functorToPresheaves_obj_map, LocallyConstant.coe_mk, Profinite.NobelingProof.GoodProducts.linearIndependent_iff_sum, LocallyConstant.congrLeftₐ_symm_apply_apply, LocallyConstant.vadd_apply, Profinite.NobelingProof.e_mem_of_eq_true, Profinite.NobelingProof.πs_apply_apply, LocallyConstant.constMonoidHom_apply, Profinite.NobelingProof.GoodProducts.finsuppSum_mem_span_eval, LocallyConstant.coe_const, Profinite.NobelingProof.GoodProducts.linearIndependent, Profinite.NobelingProof.GoodProducts.square_commutes, LocallyConstant.coe_neg, LocallyConstant.coe_one, Profinite.NobelingProof.Nobeling_aux, CompHausLike.LocallyConstantModule.functorToPresheaves_obj_obj_carrier, Profinite.NobelingProof.spanFinBasis.span, LocallyConstant.congrLeftₗ_symm_apply_apply, LocallyConstant.ker_comapₗ, TopologicalSpace.Fiber.instFiniteFiberCoeLocallyConstant, LocallyConstant.neg_apply, LocallyConstant.congrLeft_symm_apply, LocallyConstant.coe_inj, LocallyConstant.congrRightRingEquiv_apply_apply, LocallyConstant.comap_comp, LocallyConstant.mapₗ_apply_apply, LocallyConstant.congrRightRingEquiv_symm_apply_apply, Profinite.NobelingProof.GoodProducts.smaller_mono, LocallyConstant.eq_const, LocallyConstant.congrLeftₗ_apply_apply, Profinite.NobelingProof.GoodProducts.linearIndependentEmpty, LocallyConstant.map_id, LocallyConstant.mul_apply, LocallyConstant.evalₐ_apply, LocallyConstant.congr_fun, Profinite.NobelingProof.GoodProducts.span_iff_products, LocallyConstant.div_apply, LocallyConstant.coe_injective, LocallyConstant.coe_inv, Profinite.NobelingProof.GoodProducts.sum_equiv_comp_eval_eq_elim, LocallyConstant.comap_injective, LocallyConstant.comap_const, LocallyConstant.mulIndicator_of_mem, LocallyConstant.map_comp, LocallyConstant.sub_apply, LocallyConstant.constₗ_apply_apply, LocallyConstant.coe_div, TopologicalSpace.Fiber.instCompactSpaceElemValSetMemRangeCoeLocallyConstantPreimageSingleton, Profinite.NobelingProof.CC_comp_zero, LocallyConstant.coe_algebraMap, Profinite.NobelingProof.eval_eq_πJ, CompHausLike.LocallyConstant.sigmaComparison_comp_sigmaIso, Profinite.NobelingProof.Products.evalFacProp, Profinite.NobelingProof.Products.evalCons, LocallyConstant.coeFnₗ_apply, LocallyConstant.toFun_eq_coe, Profinite.NobelingProof.one_sub_e_mem_of_false, LocallyConstant.indicator_apply_eq_if, LocallyConstant.coe_add, LocallyConstant.inv_apply, Profinite.NobelingProof.injective_πs, CompHausLike.LocallyConstant.incl_comap, Profinite.NobelingProof.coe_πs', Profinite.NobelingProof.GoodProducts.range_equiv_smaller_toFun_bijective, LocallyConstant.mulIndicator_apply_eq_if, LocallyConstant.smul_apply, LocallyConstant.lift_comp_proj, Profinite.NobelingProof.list_prod_apply, LocallyConstant.comap_id, Profinite.NobelingProof.GoodProducts.linearIndependent_iff_range, LocallyConstant.coe_charFn, Profinite.NobelingProof.GoodProducts.max_eq_eval, LocallyConstant.coe_vadd, LocallyConstant.coeFnRingHom_apply, Profinite.NobelingProof.GoodProducts.linearIndependentSingleton, LocallyConstant.ofIsClopen_fiber_one, Profinite.NobelingProof.Products.eval_πs_image, Condensed.locallyConstantIsoFinYoneda_hom_app, Profinite.NobelingProof.factors_prod_eq_basis, LocallyConstant.mapAddMonoidHom_apply, LocallyConstant.coe_continuousMap, LocallyConstant.indicator_of_mem, Profinite.NobelingProof.factors_prod_eq_basis_of_eq, Profinite.NobelingProof.GoodProducts.union, LocallyConstant.toContinuousMapAlgHom_apply, LocallyConstant.congrLeft_apply, Profinite.NobelingProof.GoodProducts.max_eq_eval_unapply, CompHausLike.LocallyConstant.functorToPresheaves_obj_obj, LocallyConstant.mulIndicator_of_notMem, Profinite.NobelingProof.succ_mono, LocallyConstant.congrRight_symm_apply, LocallyConstant.comapₐ_apply_apply

---

← Back to Index