Documentation Verification Report

WithLp

📁 Source: Mathlib/Analysis/Calculus/ContDiff/WithLp.lean

Statistics

Metric	Count
Definitions	0
Theorems `contDiff_ofLp`, `contDiff_toLp`, `contDiff_ofLp`, `contDiff_toLp`, `contDiffAt_piLp`, `contDiffAt_piLp'`, `contDiffAt_piLp_apply`, `contDiffOn_piLp`, `contDiffOn_piLp'`, `contDiffOn_piLp_apply`, `contDiffWithinAt_piLp`, `contDiffWithinAt_piLp'`, `contDiffWithinAt_piLp_apply`, `contDiff_piLp`, `contDiff_piLp'`, `contDiff_piLp_apply`	16
Total	16

PiLp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`contDiff_ofLp` 📖	mathematical	—	`ContDiff` `WithLp` `normedAddCommGroup` `normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `Pi.normedAddCommGroup` `Pi.normedSpace` `WithLp.ofLp`	—	`ContinuousLinearEquiv.contDiff`
`contDiff_toLp` 📖	mathematical	—	`ContDiff` `Pi.normedAddCommGroup` `Pi.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `WithLp` `normedAddCommGroup` `normedSpace` `WithLp.toLp`	—	`ContinuousLinearEquiv.contDiff` `RingHomInvPair.ids`

WithLp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`contDiff_ofLp` 📖	mathematical	—	`ContDiff` `WithLp` `instProdNormedAddCommGroup` `instProdNormedSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NontriviallyNormedField.toNormedField` `Prod.normedAddCommGroup` `Prod.normedSpace` `ofLp`	—	`ContinuousLinearEquiv.contDiff`
`contDiff_toLp` 📖	mathematical	—	`ContDiff` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `WithLp` `instProdNormedAddCommGroup` `instProdNormedSpace` `toLp`	—	`ContinuousLinearEquiv.contDiff` `RingHomInvPair.ids`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`contDiffAt_piLp` 📖	mathematical	—	`ContDiffAt` `PiLp` `PiLp.normedAddCommGroup` `PiLp.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `WithLp.ofLp`	—	`RingHomInvPair.ids` `ContinuousLinearEquiv.comp_contDiffAt_iff` `contDiffAt_pi`
`contDiffAt_piLp'` 📖	mathematical	`ContDiffAt` `WithLp.ofLp`	`PiLp` `PiLp.normedAddCommGroup` `PiLp.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`contDiffAt_piLp`
`contDiffAt_piLp_apply` 📖	mathematical	—	`ContDiffAt` `PiLp` `PiLp.normedAddCommGroup` `PiLp.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `WithLp.ofLp`	—	`contDiffAt_piLp` `contDiffAt_id`
`contDiffOn_piLp` 📖	mathematical	—	`ContDiffOn` `PiLp` `PiLp.normedAddCommGroup` `PiLp.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `WithLp.ofLp`	—	`RingHomInvPair.ids` `ContinuousLinearEquiv.comp_contDiffOn_iff` `contDiffOn_pi`
`contDiffOn_piLp'` 📖	mathematical	`ContDiffOn` `WithLp.ofLp`	`PiLp` `PiLp.normedAddCommGroup` `PiLp.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`contDiffOn_piLp`
`contDiffOn_piLp_apply` 📖	mathematical	—	`ContDiffOn` `PiLp` `PiLp.normedAddCommGroup` `PiLp.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `WithLp.ofLp`	—	`contDiffOn_piLp` `contDiffOn_id`
`contDiffWithinAt_piLp` 📖	mathematical	—	`ContDiffWithinAt` `PiLp` `PiLp.normedAddCommGroup` `PiLp.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `WithLp.ofLp`	—	`RingHomInvPair.ids` `ContinuousLinearEquiv.comp_contDiffWithinAt_iff` `contDiffWithinAt_pi`
`contDiffWithinAt_piLp'` 📖	mathematical	`ContDiffWithinAt` `WithLp.ofLp`	`PiLp` `PiLp.normedAddCommGroup` `PiLp.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`contDiffWithinAt_piLp`
`contDiffWithinAt_piLp_apply` 📖	mathematical	—	`ContDiffWithinAt` `PiLp` `PiLp.normedAddCommGroup` `PiLp.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `WithLp.ofLp`	—	`contDiffWithinAt_piLp` `contDiffWithinAt_id`
`contDiff_piLp` 📖	mathematical	—	`ContDiff` `PiLp` `PiLp.normedAddCommGroup` `PiLp.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `WithLp.ofLp`	—	`RingHomInvPair.ids` `ContinuousLinearEquiv.comp_contDiff_iff` `contDiff_pi`
`contDiff_piLp'` 📖	mathematical	`ContDiff` `WithLp.ofLp`	`PiLp` `PiLp.normedAddCommGroup` `PiLp.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`contDiff_piLp`
`contDiff_piLp_apply` 📖	mathematical	—	`ContDiff` `PiLp` `PiLp.normedAddCommGroup` `PiLp.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `WithLp.ofLp`	—	`contDiff_piLp` `contDiff_id`

---

← Back to Index