ContinuousEval

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

Statistics

Metric	Count
Definitions ContinuousEval	1
Theorems eval, eval, continuous_eval, of_continuous_forget, toContinuousEvalConst, toContinuousMapClass, eval, eval, eval	9
Total	10

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eval 📖	mathematical	Continuous	DFunLike.coe	—	comp ContinuousEval.continuous_eval prodMk

ContinuousAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eval 📖	mathematical	ContinuousAt	DFunLike.coe	—	Filter.Tendsto.eval

ContinuousEval

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_eval 📖	mathematical	—	Continuous instTopologicalSpaceProd DFunLike.coe	—	—
of_continuous_forget 📖	mathematical	Continuous	ContinuousEval	—	Continuous.eval Continuous.fst' continuous_snd
toContinuousEvalConst 📖	mathematical	—	ContinuousEvalConst	—	Continuous.eval continuous_id continuous_const
toContinuousMapClass 📖	mathematical	—	ContinuousMapClass	—	Continuous.eval continuous_const continuous_id

ContinuousOn

Theorems

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

ContinuousWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eval 📖	mathematical	ContinuousWithinAt	DFunLike.coe	—	Filter.Tendsto.eval

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eval 📖	mathematical	Filter.Tendsto nhds	DFunLike.coe	—	comp Continuous.tendsto ContinuousEval.continuous_eval prodMk_nhds

(root)

Definitions

Name	Category	Theorems
ContinuousEval 📖	CompData	10 math math: ContinuousMapZero.instContinuousEval, ContinuousMap.instContinuousEvalOfLocallyCompactPair, GenLoop.instContinuousEval, Path.instContinuousEvalElemRealUnitInterval, ContinuousMultilinearMap.instContinuousEval, BoundedContinuousFunction.instContinuousEval, ContinuousMonoidHom.instContinuousEval, ContinuousAlternatingMap.instContinuousEval, ContinuousEval.of_continuous_forget, ContinuousAddMonoidHom.instContinuousEval

---

← Back to Index