ContinuousEvalConst

📁 Source: Mathlib/Topology/Hom/ContinuousEvalConst.lean

Statistics

Metric	Count
Definitions ContinuousEvalConst	1
Theorems coeFun, eval_const, coeFun, eval_const, continuous_eval_const, of_continuous_forget, coeFun, eval_const, coeFun, eval_const, coeFun, eval_const, continuous_coeFun	13
Total	14

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coeFun 📖	mathematical	Continuous	Pi.topologicalSpace DFunLike.coe	—	continuous_pi eval_const
eval_const 📖	mathematical	Continuous	DFunLike.coe	—	comp ContinuousEvalConst.continuous_eval_const

ContinuousAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coeFun 📖	mathematical	ContinuousAt	Pi.topologicalSpace DFunLike.coe	—	Filter.Tendsto.coeFun
eval_const 📖	mathematical	ContinuousAt	DFunLike.coe	—	Filter.Tendsto.eval_const

ContinuousEvalConst

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_eval_const 📖	mathematical	—	Continuous DFunLike.coe	—	—
of_continuous_forget 📖	mathematical	Continuous	ContinuousEvalConst	—	Continuous.comp continuous_eval_const

ContinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coeFun 📖	mathematical	ContinuousOn	DFunLike.coe	—	ContinuousWithinAt.eval_const
eval_const 📖	mathematical	ContinuousOn	DFunLike.coe	—	ContinuousWithinAt.eval_const

ContinuousWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coeFun 📖	mathematical	ContinuousWithinAt	Pi.topologicalSpace DFunLike.coe	—	Filter.Tendsto.coeFun
eval_const 📖	mathematical	ContinuousWithinAt	DFunLike.coe	—	Filter.Tendsto.eval_const

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coeFun 📖	mathematical	Filter.Tendsto nhds	DFunLike.coe Pi.topologicalSpace	—	comp Continuous.tendsto Continuous.coeFun continuous_id
eval_const 📖	mathematical	Filter.Tendsto nhds	DFunLike.coe	—	comp Continuous.tendsto Continuous.eval_const continuous_id

(root)

Definitions

Name	Category	Theorems
ContinuousEvalConst 📖	CompData	14 math math: ContinuousAddMonoidHom.instContinuousEvalConst, ContinuousLinearMap.instContinuousEvalConst, ContinuousEval.toContinuousEvalConst, ContinuousMultilinearMap.instContinuousEvalConstForall, BoundedContinuousFunction.instContinuousEvalConst, PointwiseConvergenceCLM.continuousEvalConst, ContinuousMapZero.instContinuousEvalConst, ContinuousMonoidHom.instContinuousEvalConst, ContinuousEvalConst.of_continuous_forget, UniformConvergenceCLM.continuousEvalConst, ContinuousMap.instContinuousEvalConst, CompactConvergenceCLM.instContinuousEvalConst, ContinuousAlternatingMap.instContinuousEvalConst, GenLoop.instContinuousEvalConst

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_coeFun 📖	mathematical	—	Continuous Pi.topologicalSpace DFunLike.coe	—	continuous_pi ContinuousEvalConst.continuous_eval_const

---

← Back to Index