WithLp

📁 Source: Mathlib/Analysis/Analytic/WithLp.lean

Statistics

Metric	Count
Definitions	0
Theorems analyticOn_ofLp, analyticOn_toLp, analyticOn_ofLp, analyticOn_toLp	4
Total	4

PiLp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
analyticOn_ofLp 📖	mathematical	—	AnalyticOn WithLp normedAddCommGroup normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup Pi.normedAddCommGroup Pi.normedSpace WithLp.ofLp	—	ContinuousLinearEquiv.analyticOn
analyticOn_toLp 📖	mathematical	—	AnalyticOn WithLp Pi.normedAddCommGroup Pi.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup normedAddCommGroup normedSpace WithLp.toLp	—	ContinuousLinearEquiv.analyticOn RingHomInvPair.ids

WithLp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
analyticOn_ofLp 📖	mathematical	—	AnalyticOn WithLp instProdNormedAddCommGroup instProdNormedSpace NormedAddCommGroup.toSeminormedAddCommGroup NontriviallyNormedField.toNormedField Prod.normedAddCommGroup Prod.normedSpace ofLp	—	ContinuousLinearEquiv.analyticOn
analyticOn_toLp 📖	mathematical	—	AnalyticOn WithLp Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup instProdNormedAddCommGroup instProdNormedSpace toLp	—	ContinuousLinearEquiv.analyticOn RingHomInvPair.ids

---

← Back to Index