Basic

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

Statistics

Metric	Count
Definitions `IsLocallyConstant`, `apply`, `comap`, `congrLeft`, `congrRight`, `const`, `desc`, `equivClopens`, `eval`, `flip`, `indicator`, `instCoeContinuousMap`, `instFunLike`, `instInhabited`, `map`, `mulIndicator`, `ofIsClopen`, `piecewise`, `piecewise'`, `toContinuousMap`, `toFun`, `unflip`	22
Theorems `add`, `apply_eq_of_isPreconnected`, `apply_eq_of_preconnectedSpace`, `comp`, `comp_continuous`, `comp₂`, `const`, `continuous`, `desc`, `div`, `eq_const`, `eventually_eq`, `exists_eq_const`, `exists_open`, `iff_continuous`, `iff_eventually_eq`, `iff_exists_open`, `iff_isOpen_fiber`, `iff_isOpen_fiber_apply`, `iff_is_const`, `inv`, `isClopen_fiber`, `isClosed_fiber`, `isOpen_fiber`, `mul`, `neg`, `of_constant`, `of_constant_on_connected_clopens`, `of_constant_on_connected_components`, `of_constant_on_preconnected_clopens`, `of_discrete`, `one`, `prodMk`, `range_finite`, `sub`, `zero`, `apply_eq_of_isPreconnected`, `apply_eq_of_preconnectedSpace`, `coe_comap`, `coe_comap_apply`, `coe_const`, `coe_continuousMap`, `coe_desc`, `coe_inj`, `coe_injective`, `coe_mk`, `comap_comap`, `comap_comp`, `comap_const`, `comap_id`, `comap_injective`, `congrLeft_apply`, `congrLeft_symm_apply`, `congrRight_apply`, `congrRight_symm_apply`, `congr_arg`, `congr_fun`, `continuous`, `eq_const`, `eval_apply`, `exists_eq_const`, `ext`, `ext_iff`, `flip_unflip`, `indicator_apply`, `indicator_apply_eq_if`, `indicator_of_mem`, `indicator_of_notMem`, `isLocallyConstant`, `locallyConstant_eq_of_fiber_zero_eq`, `map_apply`, `map_comp`, `map_id`, `mulIndicator_apply`, `mulIndicator_apply_eq_if`, `mulIndicator_of_mem`, `mulIndicator_of_notMem`, `ofIsClopen_fiber_one`, `ofIsClopen_fiber_zero`, `piecewise'_apply_left`, `piecewise'_apply_right`, `piecewise_apply_left`, `piecewise_apply_right`, `range_finite`, `toContinuousMap_injective`, `toFun_eq_coe`, `unflip_flip`	87
Total	109

IsLocallyConstant

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`IsLocallyConstant`	`Pi.instAdd`	—	`comp₂`
`apply_eq_of_isPreconnected` 📖	—	`IsLocallyConstant` `IsPreconnected` `Set` `Set.instMembership`	—	—	`Set.inter_compl_self` `Set.inter_empty` `Set.union_compl_self`
`apply_eq_of_preconnectedSpace` 📖	—	`IsLocallyConstant`	—	—	`apply_eq_of_isPreconnected` `PreconnectedSpace.isPreconnected_univ`
`comp` 📖	—	`IsLocallyConstant`	—	—	`Set.preimage_comp`
`comp_continuous` 📖	—	`IsLocallyConstant` `Continuous`	—	—	`Set.preimage_comp` `Continuous.isOpen_preimage`
`comp₂` 📖	—	`IsLocallyConstant`	—	—	`comp` `prodMk`
`const` 📖	mathematical	—	`IsLocallyConstant`	—	`of_constant`
`continuous` 📖	mathematical	`IsLocallyConstant`	`Continuous`	—	—
`desc` 📖	—	`IsLocallyConstant`	—	—	`Set.preimage_image_eq` `Set.preimage_preimage`
`div` 📖	mathematical	`IsLocallyConstant`	`Pi.instDiv`	—	`comp₂`
`eq_const` 📖	—	`IsLocallyConstant`	—	—	`apply_eq_of_preconnectedSpace`
`eventually_eq` 📖	mathematical	`IsLocallyConstant`	`Filter.Eventually` `nhds`	—	`iff_eventually_eq`
`exists_eq_const` 📖	—	`IsLocallyConstant`	—	—	`isEmpty_or_nonempty` `eq_const`
`exists_open` 📖	mathematical	`IsLocallyConstant`	`IsOpen` `Set` `Set.instMembership`	—	`iff_exists_open`
`iff_continuous` 📖	mathematical	—	`IsLocallyConstant` `Continuous`	—	`continuous` `Continuous.isOpen_preimage` `isOpen_discrete`
`iff_eventually_eq` 📖	mathematical	—	`IsLocallyConstant` `Filter.Eventually` `nhds`	—	`List.TFAE.out` `tfae`
`iff_exists_open` 📖	mathematical	—	`IsLocallyConstant` `IsOpen` `Set` `Set.instMembership`	—	`List.TFAE.out` `tfae`
`iff_isOpen_fiber` 📖	mathematical	—	`IsLocallyConstant` `IsOpen` `Set.preimage` `Set` `Set.instSingletonSet`	—	`List.TFAE.out` `tfae`
`iff_isOpen_fiber_apply` 📖	mathematical	—	`IsLocallyConstant` `IsOpen` `Set.preimage` `Set` `Set.instSingletonSet`	—	`List.TFAE.out` `tfae`
`iff_is_const` 📖	mathematical	—	`IsLocallyConstant`	—	`apply_eq_of_isPreconnected` `PreconnectedSpace.isPreconnected_univ` `of_constant`
`inv` 📖	mathematical	`IsLocallyConstant`	`Pi.instInv`	—	`comp`
`isClopen_fiber` 📖	mathematical	`IsLocallyConstant`	`IsClopen` `setOf`	—	`isClosed_fiber` `isOpen_fiber`
`isClosed_fiber` 📖	mathematical	`IsLocallyConstant`	`IsClosed` `setOf`	—	—
`isOpen_fiber` 📖	mathematical	`IsLocallyConstant`	`IsOpen` `setOf`	—	—
`mul` 📖	mathematical	`IsLocallyConstant`	`Pi.instMul`	—	`comp₂`
`neg` 📖	mathematical	`IsLocallyConstant`	`Pi.instNeg`	—	`comp`
`of_constant` 📖	mathematical	—	`IsLocallyConstant`	—	`iff_eventually_eq` `Filter.Eventually.of_forall`
`of_constant_on_connected_clopens` 📖	mathematical	—	`IsLocallyConstant`	—	`of_constant_on_connected_components` `isConnected_connectedComponent` `isClopen_connectedComponent` `mem_connectedComponent`
`of_constant_on_connected_components` 📖	mathematical	—	`IsLocallyConstant`	—	`iff_exists_open` `isOpen_connectedComponent` `mem_connectedComponent`
`of_constant_on_preconnected_clopens` 📖	mathematical	—	`IsLocallyConstant`	—	`of_constant_on_connected_clopens` `IsConnected.isPreconnected`
`of_discrete` 📖	mathematical	—	`IsLocallyConstant`	—	`isOpen_discrete`
`one` 📖	mathematical	—	`IsLocallyConstant` `Pi.instOne`	—	`const`
`prodMk` 📖	—	`IsLocallyConstant`	—	—	`iff_eventually_eq` `Filter.Eventually.mp` `eventually_eq` `Filter.Eventually.mono`
`range_finite` 📖	mathematical	`IsLocallyConstant`	`Set.Finite` `Set.range`	—	`IsCompact.finite_of_discrete` `discreteTopology_bot` `isCompact_range` `continuous`
`sub` 📖	mathematical	`IsLocallyConstant`	`Pi.instSub`	—	`comp₂`
`zero` 📖	mathematical	—	`IsLocallyConstant` `Pi.instZero`	—	`const`

LocallyConstant

Definitions

Name	Category	Theorems
`comap` 📖	CompOp	23 math math: `comapMonoidHom_apply`, `coe_comap_apply`, `Profinite.exists_locallyConstant_finite_aux`, `Profinite.NobelingProof.fin_comap_jointlySurjective`, `coe_comap`, `LightCondensed.isColimitLocallyConstantPresheafDiagram_desc_apply`, `comapAddMonoidHom_apply`, `Condensed.isColimitLocallyConstantPresheaf_desc_apply`, `CompHausLike.LocallyConstant.functorToPresheaves_map_app`, `comap_comap`, `Profinite.exists_locallyConstant`, `congrLeft_symm_apply`, `comap_comp`, `Condensed.isColimitLocallyConstantPresheafDiagram_desc_apply`, `comap_injective`, `comap_const`, `LightCondensed.isColimitLocallyConstantPresheaf_desc_apply`, `CompHausLike.LocallyConstant.incl_comap`, `comap_id`, `Profinite.exists_locallyConstant_finite_nonempty`, `Profinite.exists_locallyConstant_fin_two`, `CompHausLike.LocallyConstant.functorToPresheaves_obj_map`, `congrLeft_apply`
`congrLeft` 📖	CompOp	2 math math: `congrLeft_symm_apply`, `congrLeft_apply`
`congrRight` 📖	CompOp	2 math math: `congrRight_apply`, `congrRight_symm_apply`
`const` 📖	CompOp	8 math math: `exists_eq_const`, `constAddMonoidHom_apply`, `constRingHom_apply`, `constMonoidHom_apply`, `coe_const`, `eq_const`, `comap_const`, `CompHausLike.LocallyConstant.unit_app`
`desc` 📖	CompOp	1 math math: `coe_desc`
`equivClopens` 📖	CompOp	—
`eval` 📖	CompOp	1 math math: `eval_apply`
`flip` 📖	CompOp	2 math math: `unflip_flip`, `flip_unflip`
`indicator` 📖	CompOp	4 math math: `indicator_of_notMem`, `indicator_apply`, `indicator_apply_eq_if`, `indicator_of_mem`
`instCoeContinuousMap` 📖	CompOp	—
`instFunLike` 📖	CompOp	99 math math: `apply_eq_of_isPreconnected`, `congrLeftRingEquiv_apply_apply`, `coe_smul`, `charFn_eq_one`, `Profinite.NobelingProof.coe_πs`, `range_finite`, `coe_comap_apply`, `congrRightₗ_symm_apply_apply`, `zero_apply`, `comapRingHom_apply_apply`, `eval_apply`, `coe_zero`, `evalRingHom_apply`, `evalMonoidHom_apply`, `coe_sub`, `continuous`, `congrRightₐ_apply_apply`, `CompHausLike.LocallyConstant.locallyConstantIsoContinuousMap_inv_apply`, `ext_iff`, `congrRightₐ_symm_apply_apply`, `Profinite.NobelingProof.πs'_apply_apply`, `congrRightₗ_apply_apply`, `map_apply`, `congrLeftₐ_apply_apply`, `coeFnMonoidHom_apply`, `coeFnAddMonoidHom_apply`, `indicator_of_notMem`, `Profinite.NobelingProof.Products.eval_eq`, `indicator_apply`, `Profinite.NobelingProof.Products.evalFacProps`, `ofIsClopen_fiber_zero`, `mapₐ_apply_apply`, `mulIndicator_apply`, `coe_comap`, `one_apply`, `congr_arg`, `evalₗ_apply`, `constₐ_apply_apply`, `add_apply`, `charFn_eq_zero`, `Profinite.NobelingProof.factors_prod_eq_basis_of_ne`, `coeFnAlgHom_apply`, `coe_mul`, `congrLeftRingEquiv_symm_apply_apply`, `mapRingHom_apply_apply`, `evalAddMonoidHom_apply`, `apply_eq_of_preconnectedSpace`, `comapₗ_apply_apply`, `coe_mk`, `congrLeftₐ_symm_apply_apply`, `vadd_apply`, `Profinite.NobelingProof.πs_apply_apply`, `coe_const`, `coe_neg`, `coe_one`, `congrLeftₗ_symm_apply_apply`, `TopologicalSpace.Fiber.instFiniteFiberCoeLocallyConstant`, `neg_apply`, `coe_inj`, `congrRightRingEquiv_apply_apply`, `mapₗ_apply_apply`, `congrRightRingEquiv_symm_apply_apply`, `eq_const`, `congrLeftₗ_apply_apply`, `mul_apply`, `evalₐ_apply`, `congr_fun`, `div_apply`, `coe_injective`, `coe_inv`, `comap_const`, `mulIndicator_of_mem`, `sub_apply`, `constₗ_apply_apply`, `coe_div`, `TopologicalSpace.Fiber.instCompactSpaceElemValSetMemRangeCoeLocallyConstantPreimageSingleton`, `coe_algebraMap`, `CompHausLike.LocallyConstant.sigmaComparison_comp_sigmaIso`, `Profinite.NobelingProof.Products.evalFacProp`, `coeFnₗ_apply`, `toFun_eq_coe`, `indicator_apply_eq_if`, `coe_add`, `inv_apply`, `CompHausLike.LocallyConstant.incl_comap`, `mulIndicator_apply_eq_if`, `smul_apply`, `lift_comp_proj`, `Profinite.NobelingProof.list_prod_apply`, `coe_charFn`, `coe_vadd`, `coeFnRingHom_apply`, `ofIsClopen_fiber_one`, `Condensed.locallyConstantIsoFinYoneda_hom_app`, `coe_continuousMap`, `indicator_of_mem`, `Profinite.NobelingProof.factors_prod_eq_basis_of_eq`, `mulIndicator_of_notMem`, `comapₐ_apply_apply`
`instInhabited` 📖	CompOp	—
`map` 📖	CompOp	9 math math: `congrRight_apply`, `Profinite.exists_locallyConstant_finite_aux`, `map_apply`, `CompHausLike.LocallyConstant.functorToPresheaves_map_app`, `mapMonoidHom_apply`, `map_id`, `map_comp`, `mapAddMonoidHom_apply`, `congrRight_symm_apply`
`mulIndicator` 📖	CompOp	4 math math: `mulIndicator_apply`, `mulIndicator_of_mem`, `mulIndicator_apply_eq_if`, `mulIndicator_of_notMem`
`ofIsClopen` 📖	CompOp	2 math math: `ofIsClopen_fiber_zero`, `ofIsClopen_fiber_one`
`piecewise` 📖	CompOp	2 math math: `piecewise_apply_right`, `piecewise_apply_left`
`piecewise'` 📖	CompOp	2 math math: `piecewise'_apply_left`, `piecewise'_apply_right`
`toContinuousMap` 📖	CompOp	7 math math: `toContinuousMapLinearMap_apply`, `toContinuousMap_injective`, `toContinuousMapMonoidHom_apply`, `toContinuousMapAddMonoidHom_apply`, `CompHausLike.LocallyConstant.locallyConstantIsoContinuousMap_hom`, `coe_continuousMap`, `toContinuousMapAlgHom_apply`
`toFun` 📖	CompOp	3 math math: `isLocallyConstant`, `toFun_eq_coe`, `Profinite.NobelingProof.coe_πs'`
`unflip` 📖	CompOp	2 math math: `unflip_flip`, `flip_unflip`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_eq_of_isPreconnected` 📖	mathematical	`IsPreconnected` `Set` `Set.instMembership`	`DFunLike.coe` `LocallyConstant` `instFunLike`	—	`IsLocallyConstant.apply_eq_of_isPreconnected` `isLocallyConstant`
`apply_eq_of_preconnectedSpace` 📖	mathematical	—	`DFunLike.coe` `LocallyConstant` `instFunLike`	—	`IsLocallyConstant.apply_eq_of_isPreconnected` `isLocallyConstant` `PreconnectedSpace.isPreconnected_univ`
`coe_comap` 📖	mathematical	—	`DFunLike.coe` `LocallyConstant` `instFunLike` `comap` `ContinuousMap` `ContinuousMap.instFunLike`	—	—
`coe_comap_apply` 📖	mathematical	—	`DFunLike.coe` `LocallyConstant` `instFunLike` `comap` `ContinuousMap` `ContinuousMap.instFunLike`	—	—
`coe_const` 📖	mathematical	—	`DFunLike.coe` `LocallyConstant` `instFunLike` `const`	—	—
`coe_continuousMap` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `ContinuousMap.instFunLike` `toContinuousMap` `LocallyConstant` `instFunLike`	—	—
`coe_desc` 📖	mathematical	`DFunLike.coe` `LocallyConstant` `instFunLike`	`desc`	—	—
`coe_inj` 📖	mathematical	—	`DFunLike.coe` `LocallyConstant` `instFunLike`	—	`coe_injective`
`coe_injective` 📖	mathematical	—	`LocallyConstant` `DFunLike.coe` `instFunLike`	—	`DFunLike.ext'`
`coe_mk` 📖	mathematical	`IsLocallyConstant`	`DFunLike.coe` `LocallyConstant` `instFunLike`	—	—
`comap_comap` 📖	mathematical	—	`comap` `ContinuousMap.comp`	—	—
`comap_comp` 📖	mathematical	—	`comap` `ContinuousMap.comp` `LocallyConstant`	—	—
`comap_const` 📖	mathematical	`DFunLike.coe` `ContinuousMap` `ContinuousMap.instFunLike`	`comap` `const` `LocallyConstant` `instFunLike`	—	`ext`
`comap_id` 📖	mathematical	—	`comap` `ContinuousMap.id` `LocallyConstant`	—	—
`comap_injective` 📖	mathematical	`ContinuousMap.toFun`	`LocallyConstant` `comap`	—	`ext` `congr_fun`
`congrLeft_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `LocallyConstant` `EquivLike.toFunLike` `Equiv.instEquivLike` `congrLeft` `comap` `toContinuousMap` `Homeomorph` `Homeomorph.instEquivLike` `Homeomorph.instContinuousMapClass` `Homeomorph.symm`	—	—
`congrLeft_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `LocallyConstant` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `congrLeft` `comap` `toContinuousMap` `Homeomorph` `Homeomorph.instEquivLike` `Homeomorph.instContinuousMapClass`	—	—
`congrRight_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `LocallyConstant` `EquivLike.toFunLike` `Equiv.instEquivLike` `congrRight` `map`	—	—
`congrRight_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `LocallyConstant` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `congrRight` `map`	—	—
`congr_arg` 📖	mathematical	—	`DFunLike.coe` `LocallyConstant` `instFunLike`	—	`DFunLike.congr_arg`
`congr_fun` 📖	mathematical	—	`DFunLike.coe` `LocallyConstant` `instFunLike`	—	`DFunLike.congr_fun`
`continuous` 📖	mathematical	—	`Continuous` `DFunLike.coe` `LocallyConstant` `instFunLike`	—	`IsLocallyConstant.continuous` `isLocallyConstant`
`eq_const` 📖	mathematical	—	`const` `DFunLike.coe` `LocallyConstant` `instFunLike`	—	`ext` `apply_eq_of_preconnectedSpace`
`eval_apply` 📖	mathematical	—	`DFunLike.coe` `LocallyConstant` `Pi.topologicalSpace` `instFunLike` `eval`	—	—
`exists_eq_const` 📖	mathematical	—	`const`	—	`eq_const` `ext`
`ext` 📖	—	`DFunLike.coe` `LocallyConstant` `instFunLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `LocallyConstant` `instFunLike`	—	`ext`
`flip_unflip` 📖	mathematical	—	`flip` `unflip`	—	—
`indicator_apply` 📖	mathematical	`IsClopen`	`DFunLike.coe` `LocallyConstant` `instFunLike` `indicator` `Set.indicator`	—	—
`indicator_apply_eq_if` 📖	mathematical	`IsClopen`	`DFunLike.coe` `LocallyConstant` `instFunLike` `indicator` `Set` `Set.instMembership`	—	`Set.indicator_apply`
`indicator_of_mem` 📖	mathematical	`IsClopen` `Set` `Set.instMembership`	`DFunLike.coe` `LocallyConstant` `instFunLike` `indicator`	—	`Set.indicator_of_mem`
`indicator_of_notMem` 📖	mathematical	`IsClopen` `Set` `Set.instMembership`	`DFunLike.coe` `LocallyConstant` `instFunLike` `indicator`	—	`Set.indicator_of_notMem`
`isLocallyConstant` 📖	mathematical	—	`IsLocallyConstant` `toFun`	—	—
`locallyConstant_eq_of_fiber_zero_eq` 📖	—	`Set.preimage` `DFunLike.coe` `LocallyConstant` `instFunLike` `Set` `Set.instSingletonSet`	—	—	`ext`
`map_apply` 📖	mathematical	—	`DFunLike.coe` `LocallyConstant` `instFunLike` `map`	—	—
`map_comp` 📖	mathematical	—	`LocallyConstant` `map`	—	—
`map_id` 📖	mathematical	—	`map` `LocallyConstant`	—	—
`mulIndicator_apply` 📖	mathematical	`IsClopen`	`DFunLike.coe` `LocallyConstant` `instFunLike` `mulIndicator` `Set.mulIndicator`	—	—
`mulIndicator_apply_eq_if` 📖	mathematical	`IsClopen`	`DFunLike.coe` `LocallyConstant` `instFunLike` `mulIndicator` `Set` `Set.instMembership`	—	`Set.mulIndicator_apply`
`mulIndicator_of_mem` 📖	mathematical	`IsClopen` `Set` `Set.instMembership`	`DFunLike.coe` `LocallyConstant` `instFunLike` `mulIndicator`	—	`Set.mulIndicator_of_mem`
`mulIndicator_of_notMem` 📖	mathematical	`IsClopen` `Set` `Set.instMembership`	`DFunLike.coe` `LocallyConstant` `instFunLike` `mulIndicator`	—	`Set.mulIndicator_of_notMem`
`ofIsClopen_fiber_one` 📖	mathematical	`IsClopen`	`Set.preimage` `DFunLike.coe` `LocallyConstant` `instFunLike` `ofIsClopen` `Set` `Set.instSingletonSet` `Compl.compl` `Set.instCompl`	—	`Set.ext`
`ofIsClopen_fiber_zero` 📖	mathematical	`IsClopen`	`Set.preimage` `DFunLike.coe` `LocallyConstant` `instFunLike` `ofIsClopen` `Set` `Set.instSingletonSet`	—	`Set.ext`
`piecewise'_apply_left` 📖	mathematical	`Set` `Set.instHasSubset` `Set.instUnion` `DFunLike.coe` `LocallyConstant` `Set.Elem` `instTopologicalSpaceSubtype` `Set.instMembership` `instFunLike`	`piecewise'`	—	`piecewise'.eq_1` `Continuous.restrictPreimage` `continuous_subtype_val` `piecewise_apply_left`
`piecewise'_apply_right` 📖	mathematical	`Set` `Set.instHasSubset` `Set.instUnion` `DFunLike.coe` `LocallyConstant` `Set.Elem` `instTopologicalSpaceSubtype` `Set.instMembership` `instFunLike`	`piecewise'`	—	`piecewise'.eq_1` `Continuous.restrictPreimage` `continuous_subtype_val` `piecewise_apply_right`
`piecewise_apply_left` 📖	mathematical	`Set` `Set.instUnion` `Set.univ` `DFunLike.coe` `LocallyConstant` `Set.Elem` `instTopologicalSpaceSubtype` `Set.instMembership` `instFunLike`	`piecewise`	—	—
`piecewise_apply_right` 📖	mathematical	`Set` `Set.instUnion` `Set.univ` `DFunLike.coe` `LocallyConstant` `Set.Elem` `instTopologicalSpaceSubtype` `Set.instMembership` `instFunLike`	`piecewise`	—	—
`range_finite` 📖	mathematical	—	`Set.Finite` `Set.range` `DFunLike.coe` `LocallyConstant` `instFunLike`	—	`IsLocallyConstant.range_finite` `isLocallyConstant`
`toContinuousMap_injective` 📖	mathematical	—	`LocallyConstant` `ContinuousMap` `toContinuousMap`	—	`ext` `ContinuousMap.congr_fun`
`toFun_eq_coe` 📖	mathematical	—	`toFun` `DFunLike.coe` `LocallyConstant` `instFunLike`	—	—
`unflip_flip` 📖	mathematical	—	`unflip` `flip`	—	—

LocallyConstant.Simps

Definitions

Name	Category	Theorems
`apply` 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
`IsLocallyConstant` 📖	MathDef	22 math math: `IsLocallyConstant.iff_exists_open`, `IsLocallyConstant.one`, `IsLocallyConstant.iff_eventually_eq`, `IsLocallyConstant.iff_continuous`, `LocallyConstant.isLocallyConstant`, `IsLocallyConstant.of_constant_on_connected_clopens`, `Module.isLocallyConstant_rankAtStalk_freeLocus`, `IsLocallyConstant.const`, `MDifferentiable.isLocallyConstant`, `IsLocallyConstant.tfae`, `IsLocallyConstant.zero`, `IsLocallyConstant.of_discrete`, `Module.isLocallyConstant_rankAtStalk`, `IsLocallyConstant.of_constant_on_connected_components`, `DiscreteQuotient.proj_isLocallyConstant`, `isLocallyConstant_of_fderiv_eq_zero`, `IsLocallyConstant.of_constant_on_preconnected_clopens`, `IsLocallyConstant.of_germ_isConstant`, `IsLocallyConstant.of_constant`, `IsLocallyConstant.iff_isOpen_fiber`, `IsLocallyConstant.iff_is_const`, `IsLocallyConstant.iff_isOpen_fiber_apply`

---

← Back to Index