FDerivCurry

📁 Source: PhysLean/Mathematics/FDerivCurry.lean

Statistics

Metric	Count
Definitions	0
Theorems `fderiv_curry_clm_apply`, `fderiv_curry_comp_fst`, `fderiv_curry_comp_snd`, `fderiv_curry_differentiableAt_fst_comp_snd`, `fderiv_curry_differentiableAt_snd_comp_fst`, `fderiv_curry_fst`, `fderiv_curry_snd`, `fderiv_inl_snd_clm`, `fderiv_inr_fst_clm`, `fderiv_swap`, `fderiv_uncurry`, `fderiv_uncurry_clm_comp`, `fderiv_uncurry_comp_fst`, `fderiv_uncurry_comp_snd`, `fderiv_uncurry_differentiable_fst`, `fderiv_uncurry_differentiable_fst_comp_snd`, `fderiv_uncurry_differentiable_fst_comp_snd_apply`, `fderiv_uncurry_differentiable_snd`, `fderiv_uncurry_differentiable_snd_comp_fst`, `fderiv_uncurry_differentiable_snd_comp_fst_apply`, `fderiv_wrt_prod`, `fderiv_wrt_prod_clm_comp`, `function_differentiableAt_fst`, `function_differentiableAt_snd`	24
Total	24

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fderiv_curry_clm_apply` 📖	—	—	—	—	—
`fderiv_curry_comp_fst` 📖	—	—	—	—	—
`fderiv_curry_comp_snd` 📖	—	—	—	—	—
`fderiv_curry_differentiableAt_fst_comp_snd` 📖	—	—	—	—	`fderiv_uncurry_differentiable_fst_comp_snd_apply`
`fderiv_curry_differentiableAt_snd_comp_fst` 📖	—	—	—	—	`fderiv_uncurry_differentiable_snd_comp_fst_apply`
`fderiv_curry_fst` 📖	—	—	—	—	`fderiv_uncurry`
`fderiv_curry_snd` 📖	—	—	—	—	`fderiv_uncurry`
`fderiv_inl_snd_clm` 📖	—	—	—	—	—
`fderiv_inr_fst_clm` 📖	—	—	—	—	—
`fderiv_swap` 📖	—	—	—	—	`fderiv_curry_clm_apply` `fderiv_uncurry_differentiable_fst_comp_snd` `fderiv_uncurry_differentiable_snd` `fderiv_uncurry_differentiable_fst` `fderiv_uncurry_differentiable_snd_comp_fst` `fderiv_wrt_prod_clm_comp`
`fderiv_uncurry` 📖	—	—	—	—	—
`fderiv_uncurry_clm_comp` 📖	—	—	—	—	`fderiv_uncurry`
`fderiv_uncurry_comp_fst` 📖	—	—	—	—	—
`fderiv_uncurry_comp_snd` 📖	—	—	—	—	—
`fderiv_uncurry_differentiable_fst` 📖	—	—	—	—	—
`fderiv_uncurry_differentiable_fst_comp_snd` 📖	—	—	—	—	—
`fderiv_uncurry_differentiable_fst_comp_snd_apply` 📖	—	—	—	—	`fderiv_uncurry_differentiable_fst_comp_snd`
`fderiv_uncurry_differentiable_snd` 📖	—	—	—	—	—
`fderiv_uncurry_differentiable_snd_comp_fst` 📖	—	—	—	—	—
`fderiv_uncurry_differentiable_snd_comp_fst_apply` 📖	—	—	—	—	`fderiv_uncurry_differentiable_snd_comp_fst`
`fderiv_wrt_prod` 📖	—	—	—	—	`fderiv_uncurry`
`fderiv_wrt_prod_clm_comp` 📖	—	—	—	—	`fderiv_uncurry_clm_comp`
`function_differentiableAt_fst` 📖	—	—	—	—	—
`function_differentiableAt_snd` 📖	—	—	—	—	—

---

← Back to Index