Comp

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

Statistics

Metric	Count
Definitions	0
Theorems `clm_apply`, `clm_comp`, `comp`, `comp_contDiffAt`, `comp_contDiffOn`, `comp_contDiffWithinAt`, `comp₂`, `comp₂_contDiffAt`, `comp₂_contDiffOn`, `comp₂_contDiffWithinAt`, `comp₃`, `comp₃_contDiffOn`, `contDiff_fderiv_apply`, `fderiv`, `fderiv_apply`, `fderiv_right`, `fderiv_succ`, `fst`, `fst'`, `fun_comp`, `fun_comp_contDiffOn`, `iteratedFDeriv_right`, `iteratedFDeriv_right'`, `smulRight`, `snd`, `snd'`, `clm_apply`, `clm_comp`, `comp`, `comp_contDiffWithinAt`, `comp_contDiffWithinAt_of_eq`, `comp₂`, `comp₂_contDiffWithinAt`, `continuousAt_fderiv`, `continuousAt_iteratedFDeriv`, `fderiv`, `fderiv_right`, `fderiv_right_succ`, `fderiv_succ`, `fst`, `fst'`, `fst''`, `fun_comp`, `iteratedFDeriv_right`, `smulRight`, `snd`, `snd'`, `snd''`, `clm_apply`, `clm_comp`, `comp`, `comp_contDiff`, `comp_inter`, `continuousOn_fderivWithin_apply`, `fst`, `image_comp_contDiff`, `smulRight`, `snd`, `clm_apply`, `clm_comp`, `comp`, `comp_inter`, `comp_inter_of_eq`, `comp_of_eq`, `comp_of_mem_nhdsWithin_image`, `comp_of_mem_nhdsWithin_image_of_eq`, `comp_of_preimage_mem_nhdsWithin`, `comp_of_preimage_mem_nhdsWithin_of_eq`, `continuousWithinAt_fderivWithin`, `continuousWithinAt_iteratedFDerivWithin`, `fderivWithin`, `fderivWithin'`, `fderivWithin''`, `fderivWithin_apply`, `fderivWithin_right`, `fderivWithin_right_apply`, `hasFDerivWithinAt_nhds`, `iteratedFDerivWithin_right`, `smulRight`, `fderiv`, `fderiv_one`, `continuousOn_iteratedFDeriv`, `continuousOn_iteratedFDerivWithin`, `fderiv_two`, `contDiffAt_fst`, `contDiffAt_snd`, `contDiffOn_fderivWithin_apply`, `contDiffOn_fst`, `contDiffOn_snd`, `contDiffWithinAt_fst`, `contDiffWithinAt_snd`, `contDiff_fst`, `contDiff_snd`, `iteratedFDerivWithin_clm_apply_const_apply`, `iteratedFDerivWithin_comp`, `iteratedFDerivWithin_comp_of_eventually_mem`, `iteratedFDeriv_clm_apply_const_apply`, `iteratedFDeriv_comp`	98
Total	98

ContDiff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`clm_apply` 📖	mathematical	`ContDiff` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContinuousLinearMap.toNormedSpace` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing`	`DFunLike.coe` `ContinuousLinearMap.funLike`	—	`RingHomIsometric.ids` `smulCommClass_self` `comp₂` `IsBoundedBilinearMap.contDiff` `isBoundedBilinearMap_apply`
`clm_comp` 📖	mathematical	`ContDiff` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContinuousLinearMap.toNormedSpace` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing`	`ContinuousLinearMap.comp` `RingHomCompTriple.ids`	—	`RingHomIsometric.ids` `smulCommClass_self` `comp₂` `RingHomCompTriple.ids` `IsBoundedBilinearMap.contDiff` `isBoundedBilinearMap_comp`
`comp` 📖	—	`ContDiff`	—	—	`contDiffOn_univ` `ContDiffOn.comp` `Set.subset_univ`
`comp_contDiffAt` 📖	—	`ContDiff` `ContDiffAt`	—	—	`comp_contDiffWithinAt`
`comp_contDiffOn` 📖	—	`ContDiff` `ContDiffOn`	—	—	`ContDiffOn.comp` `contDiffOn_univ` `Set.mapsTo_univ`
`comp_contDiffWithinAt` 📖	—	`ContDiff` `ContDiffWithinAt`	—	—	`ContDiffWithinAt.comp` `ContDiffAt.contDiffWithinAt` `contDiffAt` `Set.subset_univ`
`comp₂` 📖	—	`ContDiff` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	—	`comp` `prodMk`
`comp₂_contDiffAt` 📖	—	`ContDiff` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ContDiffAt`	—	—	`ContDiffAt.comp₂` `contDiffAt`
`comp₂_contDiffOn` 📖	—	`ContDiff` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ContDiffOn`	—	—	`comp_contDiffOn` `ContDiffOn.prodMk`
`comp₂_contDiffWithinAt` 📖	—	`ContDiff` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ContDiffWithinAt`	—	—	`ContDiffAt.comp_contDiffWithinAt` `contDiffAt` `ContDiffWithinAt.prodMk`
`comp₃` 📖	—	`ContDiff` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	—	`comp₂` `prodMk`
`comp₃_contDiffOn` 📖	—	`ContDiff` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ContDiffOn`	—	—	`comp₂_contDiffOn` `ContDiffOn.prodMk`
`contDiff_fderiv_apply` 📖	mathematical	`ContDiff` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `WithTop.add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	`Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `ContinuousLinearMap.funLike` `fderiv`	—	`contDiffOn_univ` `fderivWithin_univ` `Set.univ_prod_univ` `contDiffOn_fderivWithin_apply` `uniqueDiffOn_univ` `NormedField.nhdsNE_neBot` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul`
`fderiv` 📖	mathematical	`ContDiff` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `WithTop.add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	`ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContinuousLinearMap.toNormedSpace` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `fderiv`	—	`RingHomIsometric.ids` `smulCommClass_self` `contDiff_iff_contDiffAt` `ContDiffAt.fderiv` `contDiffAt`
`fderiv_apply` 📖	mathematical	`ContDiff` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `WithTop.add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	`DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `ContinuousLinearMap.funLike` `fderiv`	—	`clm_apply` `fderiv`
`fderiv_right` 📖	mathematical	`ContDiff` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `WithTop.add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	`ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContinuousLinearMap.toNormedSpace` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `fderiv`	—	`RingHomIsometric.ids` `smulCommClass_self` `contDiff_iff_contDiffAt` `ContDiffAt.fderiv_right` `contDiffAt`
`fderiv_succ` 📖	mathematical	`ContDiff` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `WithTop` `ENat` `WithTop.add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	`ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContinuousLinearMap.toNormedSpace` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `fderiv`	—	`RingHomIsometric.ids` `smulCommClass_self` `contDiff_iff_contDiffAt` `ContDiffAt.fderiv` `contDiffAt` `le_refl`
`fst` 📖	—	`ContDiff` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	—	`comp` `contDiff_fst`
`fst'` 📖	mathematical	`ContDiff`	`Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`comp` `contDiff_fst`
`fun_comp` 📖	—	`ContDiff`	—	—	`comp`
`fun_comp_contDiffOn` 📖	—	`ContDiff` `ContDiffOn`	—	—	`ContDiffOn.comp` `contDiffOn_univ` `Set.mapsTo_univ`
`iteratedFDeriv_right` 📖	mathematical	`ContDiff` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `WithTop.add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `AddMonoidWithOne.toNatCast` `WithTop.addMonoidWithOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	`ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousMultilinearMap.normedAddCommGroup'` `Fin.fintype` `ContinuousMultilinearMap.normedSpace'` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `iteratedFDeriv`	—	`smulCommClass_self` `contDiff_iff_contDiffAt` `ContDiffAt.iteratedFDeriv_right` `contDiffAt`
`iteratedFDeriv_right'` 📖	mathematical	`ContDiff` `WithTop` `ENat` `WithTop.add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `AddMonoidWithOne.toNatCast` `WithTop.addMonoidWithOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	`ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousMultilinearMap.normedAddCommGroup'` `Fin.fintype` `ContinuousMultilinearMap.normedSpace'` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `iteratedFDeriv`	—	`smulCommClass_self` `contDiff_iff_contDiffAt` `ContDiffAt.iteratedFDeriv_right` `contDiffAt` `le_refl`
`smulRight` 📖	mathematical	`ContDiff` `StrongDual` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `ContinuousLinearMap.toNormedAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedSpace` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomIsometric.ids` `ContinuousLinearMap.toNormedSpace` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `Algebra.to_smulCommClass` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id`	`ContinuousLinearMap` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `ContinuousLinearMap.smulRight` `Semiring.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IsBoundedSMul.continuousSMul` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `NormedSpace.toIsBoundedSMul`	—	`RingHomIsometric.ids` `Algebra.to_smulCommClass` `comp₂` `smulCommClass_self` `IsScalarTower.left` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `IsBoundedBilinearMap.contDiff` `isBoundedBilinearMap_smulRight`
`snd` 📖	—	`ContDiff` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	—	`comp` `contDiff_snd`
`snd'` 📖	mathematical	`ContDiff`	`Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`comp` `contDiff_snd`

ContDiffAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`clm_apply` 📖	mathematical	`ContDiffAt` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContinuousLinearMap.toNormedSpace` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing`	`DFunLike.coe` `ContinuousLinearMap.funLike`	—	`RingHomIsometric.ids` `smulCommClass_self` `ContDiff.comp₂_contDiffAt` `IsBoundedBilinearMap.contDiff` `isBoundedBilinearMap_apply`
`clm_comp` 📖	mathematical	`ContDiffAt` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContinuousLinearMap.toNormedSpace` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing`	`ContinuousLinearMap.comp` `RingHomCompTriple.ids`	—	`RingHomIsometric.ids` `smulCommClass_self` `ContDiff.comp₂_contDiffAt` `RingHomCompTriple.ids` `IsBoundedBilinearMap.contDiff` `isBoundedBilinearMap_comp`
`comp` 📖	—	`ContDiffAt`	—	—	`ContDiffWithinAt.comp` `Set.mapsTo_univ`
`comp_contDiffWithinAt` 📖	—	`ContDiffAt` `ContDiffWithinAt`	—	—	`ContDiffWithinAt.comp` `Set.mapsTo_univ`
`comp_contDiffWithinAt_of_eq` 📖	—	`ContDiffAt` `ContDiffWithinAt`	—	—	`comp_contDiffWithinAt`
`comp₂` 📖	—	`ContDiffAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	—	`comp` `prodMk`
`comp₂_contDiffWithinAt` 📖	—	`ContDiffAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ContDiffWithinAt`	—	—	`comp_contDiffWithinAt` `ContDiffWithinAt.prodMk`
`continuousAt_fderiv` 📖	mathematical	`ContDiffAt`	`ContinuousAt` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `ContinuousLinearMap.topologicalSpace` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `fderiv`	—	`continuousAt` `RingHomIsometric.ids` `smulCommClass_self` `fderiv_right` `zero_add`
`continuousAt_iteratedFDeriv` 📖	mathematical	`ContDiffAt` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `AddMonoidWithOne.toNatCast` `WithTop.addMonoidWithOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	`ContinuousAt` `ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousMultilinearMap.instTopologicalSpace` `NormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `iteratedFDeriv`	—	`continuousAt` `smulCommClass_self` `iteratedFDeriv_right` `zero_add`
`fderiv` 📖	mathematical	`ContDiffAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `WithTop.add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	`ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContinuousLinearMap.toNormedSpace` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `fderiv`	—	`RingHomIsometric.ids` `smulCommClass_self` `ContDiffWithinAt.contDiffAt` `ContDiffWithinAt.fderivWithin` `contDiffWithinAt` `uniqueDiffOn_univ` `NormedField.nhdsNE_neBot` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `Set.mem_univ` `Set.preimage_univ` `subset_refl` `Set.instReflSubset` `Filter.univ_mem`
`fderiv_right` 📖	mathematical	`ContDiffAt` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `WithTop.add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	`ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContinuousLinearMap.toNormedSpace` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `fderiv`	—	`fderiv` `comp` `contDiffAt_snd` `contDiffAt_id`
`fderiv_right_succ` 📖	mathematical	`ContDiffAt` `WithTop` `ENat` `WithTop.add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	`ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContinuousLinearMap.toNormedSpace` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `fderiv`	—	`fderiv` `comp` `contDiffAt_snd` `contDiffAt_id` `le_refl`
`fderiv_succ` 📖	mathematical	`ContDiffAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `WithTop` `ENat` `WithTop.add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	`ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContinuousLinearMap.toNormedSpace` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `fderiv`	—	`fderiv` `le_refl`
`fst` 📖	—	`ContDiffAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	—	`comp` `contDiffAt_fst`
`fst'` 📖	mathematical	`ContDiffAt`	`Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`comp` `contDiffAt_fst`
`fst''` 📖	mathematical	`ContDiffAt`	`Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`comp` `contDiffAt_fst`
`fun_comp` 📖	—	`ContDiffAt`	—	—	`comp`
`iteratedFDeriv_right` 📖	mathematical	`ContDiffAt` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `WithTop.add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `AddMonoidWithOne.toNatCast` `WithTop.addMonoidWithOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	`ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousMultilinearMap.normedAddCommGroup'` `Fin.fintype` `ContinuousMultilinearMap.normedSpace'` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `iteratedFDeriv`	—	`smulCommClass_self` `iteratedFDerivWithin_univ` `contDiffWithinAt_univ` `ContDiffWithinAt.iteratedFDerivWithin_right` `uniqueDiffOn_univ` `NormedField.nhdsNE_neBot` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul`
`smulRight` 📖	mathematical	`ContDiffAt` `StrongDual` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `ContinuousLinearMap.toNormedAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedSpace` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomIsometric.ids` `ContinuousLinearMap.toNormedSpace` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `Algebra.to_smulCommClass` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id`	`ContinuousLinearMap` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `ContinuousLinearMap.smulRight` `Semiring.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IsBoundedSMul.continuousSMul` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `NormedSpace.toIsBoundedSMul`	—	`RingHomIsometric.ids` `Algebra.to_smulCommClass` `ContDiff.comp₂_contDiffAt` `smulCommClass_self` `IsScalarTower.left` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `IsBoundedBilinearMap.contDiff` `isBoundedBilinearMap_smulRight`
`snd` 📖	—	`ContDiffAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	—	`comp` `contDiffAt_snd`
`snd'` 📖	mathematical	`ContDiffAt`	`Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`comp` `contDiffAt_snd`
`snd''` 📖	mathematical	`ContDiffAt`	`Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`comp` `contDiffAt_snd`

ContDiffOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`clm_apply` 📖	mathematical	`ContDiffOn` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContinuousLinearMap.toNormedSpace` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing`	`DFunLike.coe` `ContinuousLinearMap.funLike`	—	`RingHomIsometric.ids` `smulCommClass_self` `ContDiff.comp₂_contDiffOn` `IsBoundedBilinearMap.contDiff` `isBoundedBilinearMap_apply`
`clm_comp` 📖	mathematical	`ContDiffOn` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContinuousLinearMap.toNormedSpace` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing`	`ContinuousLinearMap.comp` `RingHomCompTriple.ids`	—	`RingHomIsometric.ids` `smulCommClass_self` `ContDiff.comp₂_contDiffOn` `RingHomCompTriple.ids` `IsBoundedBilinearMap.contDiff` `isBoundedBilinearMap_comp`
`comp` 📖	—	`ContDiffOn` `Set.MapsTo`	—	—	`ContDiffWithinAt.comp`
`comp_contDiff` 📖	—	`ContDiffOn` `ContDiff` `Set` `Set.instMembership`	—	—	`contDiffOn_univ` `comp`
`comp_inter` 📖	mathematical	`ContDiffOn`	`Set` `Set.instInter` `Set.preimage`	—	`comp` `mono` `Set.inter_subset_left` `Set.inter_subset_right`
`continuousOn_fderivWithin_apply` 📖	mathematical	`ContDiffOn` `UniqueDiffOn` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	`ContinuousOn` `instTopologicalSpaceProd` `DFunLike.coe` `ContinuousLinearMap` `RingHom.id` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.funLike` `fderivWithin` `SProd.sprod` `Set` `Set.instSProd` `Set.univ`	—	`continuousOn` `contDiffOn_fderivWithin_apply`
`fst` 📖	—	`ContDiffOn` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	—	`ContDiff.comp_contDiffOn` `contDiff_fst`
`image_comp_contDiff` 📖	—	`ContDiffOn` `Set.image` `ContDiff`	—	—	`comp` `ContDiff.contDiffOn` `Set.mapsTo_image`
`smulRight` 📖	mathematical	`ContDiffOn` `StrongDual` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `ContinuousLinearMap.toNormedAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedSpace` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomIsometric.ids` `ContinuousLinearMap.toNormedSpace` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `Algebra.to_smulCommClass` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id`	`ContinuousLinearMap` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `ContinuousLinearMap.smulRight` `Semiring.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IsBoundedSMul.continuousSMul` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `NormedSpace.toIsBoundedSMul`	—	`RingHomIsometric.ids` `Algebra.to_smulCommClass` `ContDiff.comp₂_contDiffOn` `smulCommClass_self` `IsScalarTower.left` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `IsBoundedBilinearMap.contDiff` `isBoundedBilinearMap_smulRight`
`snd` 📖	—	`ContDiffOn` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	—	`ContDiff.comp_contDiffOn` `contDiff_snd`

ContDiffWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`clm_apply` 📖	mathematical	`ContDiffWithinAt` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContinuousLinearMap.toNormedSpace` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing`	`DFunLike.coe` `ContinuousLinearMap.funLike`	—	`RingHomIsometric.ids` `smulCommClass_self` `ContDiff.comp₂_contDiffWithinAt` `IsBoundedBilinearMap.contDiff` `isBoundedBilinearMap_apply`
`clm_comp` 📖	mathematical	`ContDiffWithinAt` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContinuousLinearMap.toNormedSpace` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing`	`ContinuousLinearMap.comp` `RingHomCompTriple.ids`	—	`RingHomIsometric.ids` `smulCommClass_self` `ContDiff.comp₂_contDiffWithinAt` `RingHomCompTriple.ids` `IsBoundedBilinearMap.contDiff` `isBoundedBilinearMap_comp`
`comp` 📖	—	`ContDiffWithinAt` `Set.MapsTo`	—	—	`Filter.inter_mem` `self_mem_nhdsWithin` `ContinuousWithinAt.preimage_mem_nhdsWithin'` `continuousWithinAt_insert_self` `continuousWithinAt` `nhdsWithin_mono` `Set.image_insert_eq` `Set.insert_subset_insert` `Set.image_subset_iff` `HasFTaylorSeriesUpToOn.comp` `HasFTaylorSeriesUpToOn.mono` `smulCommClass_self` `RingHomInvPair.ids` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `AnalyticOn.congr` `AnalyticOn.mono` `HasFTaylorSeriesUpToOn.zero_eq'` `AnalyticOnNhd.comp_analyticOn` `LinearIsometryEquiv.analyticOnNhd` `Set.mapsTo_univ` `LinearIsometryEquiv.apply_symm_apply` `analyticOn_taylorComp`
`comp_inter` 📖	mathematical	`ContDiffWithinAt`	`Set` `Set.instInter` `Set.preimage`	—	`comp` `mono` `Set.inter_subset_left` `Set.inter_subset_right`
`comp_inter_of_eq` 📖	mathematical	`ContDiffWithinAt`	`Set` `Set.instInter` `Set.preimage`	—	`comp_inter`
`comp_of_eq` 📖	—	`ContDiffWithinAt` `Set.MapsTo`	—	—	`comp`
`comp_of_mem_nhdsWithin_image` 📖	—	`ContDiffWithinAt` `Set` `Filter` `Filter.instMembership` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set.image`	—	—	`comp` `mono_of_mem_nhdsWithin` `Set.subset_preimage_image`
`comp_of_mem_nhdsWithin_image_of_eq` 📖	—	`ContDiffWithinAt` `Set` `Filter` `Filter.instMembership` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set.image`	—	—	`comp_of_mem_nhdsWithin_image`
`comp_of_preimage_mem_nhdsWithin` 📖	—	`ContDiffWithinAt` `Set` `Filter` `Filter.instMembership` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set.preimage`	—	—	`mono_of_mem_nhdsWithin` `comp_inter` `Filter.inter_mem` `self_mem_nhdsWithin`
`comp_of_preimage_mem_nhdsWithin_of_eq` 📖	—	`ContDiffWithinAt` `Set` `Filter` `Filter.instMembership` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set.preimage`	—	—	`comp_of_preimage_mem_nhdsWithin`
`continuousWithinAt_fderivWithin` 📖	mathematical	`ContDiffWithinAt` `UniqueDiffOn` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Set` `Set.instMembership`	`ContinuousWithinAt` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.topologicalSpace` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `fderivWithin`	—	`continuousWithinAt` `RingHomIsometric.ids` `smulCommClass_self` `fderivWithin_right` `zero_add`
`continuousWithinAt_iteratedFDerivWithin` 📖	mathematical	`ContDiffWithinAt` `UniqueDiffOn` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `AddMonoidWithOne.toNatCast` `WithTop.addMonoidWithOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `Set` `Set.instMembership`	`ContinuousWithinAt` `ContinuousMultilinearMap` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousMultilinearMap.instTopologicalSpace` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `iteratedFDerivWithin`	—	`continuousWithinAt` `smulCommClass_self` `iteratedFDerivWithin_right` `zero_add`
`fderivWithin` 📖	mathematical	`ContDiffWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `SProd.sprod` `Set` `Set.instSProd` `UniqueDiffOn` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `WithTop.add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Set.instMembership` `Set.instHasSubset` `Set.preimage`	`ContinuousLinearMap` `RingHom.id` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContinuousLinearMap.toNormedSpace` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `fderivWithin`	—	`fderivWithin'` `Set.insert_eq_self` `Filter.eventually_of_mem` `self_mem_nhdsWithin`
`fderivWithin'` 📖	mathematical	`ContDiffWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `SProd.sprod` `Set` `Set.instSProd` `Set.instInsert` `Filter.Eventually` `UniqueDiffWithinAt` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `nhdsWithin` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `WithTop.add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Set.instHasSubset` `Set.preimage`	`ContinuousLinearMap` `RingHom.id` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContinuousLinearMap.toNormedSpace` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `fderivWithin`	—	`fderivWithin''` `Filter.mem_of_superset` `self_mem_nhdsWithin` `Set.image_subset_iff`
`fderivWithin''` 📖	mathematical	`ContDiffWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `SProd.sprod` `Set` `Set.instSProd` `Set.instInsert` `Filter.Eventually` `UniqueDiffWithinAt` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `nhdsWithin` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `WithTop.add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Filter` `Filter.instMembership` `Set.image`	`ContinuousLinearMap` `RingHom.id` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContinuousLinearMap.toNormedSpace` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `fderivWithin`	—	`RingHomIsometric.ids` `smulCommClass_self` `hasFDerivWithinAt_nhds` `of_le` `le_imp_le_of_le_of_le` `add_le_add_left` `WithTop.addRightMono` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid` `le_refl` `congr_of_eventuallyEq_insert` `Filter.mp_mem` `Filter.univ_mem'` `HasFDerivWithinAt.fderivWithin` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `contDiffWithinAt_infty` `le_top` `le_rfl`
`fderivWithin_apply` 📖	mathematical	`ContDiffWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `SProd.sprod` `Set` `Set.instSProd` `UniqueDiffOn` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `WithTop.add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Set.instMembership` `Set.instHasSubset` `Set.preimage`	`DFunLike.coe` `ContinuousLinearMap` `RingHom.id` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.funLike` `fderivWithin`	—	`ContDiffAt.comp_contDiffWithinAt` `RingHomIsometric.ids` `smulCommClass_self` `ContDiff.contDiffAt` `ContDiff.clm_apply` `contDiff_fst` `contDiff_snd` `prodMk` `fderivWithin`
`fderivWithin_right` 📖	mathematical	`ContDiffWithinAt` `UniqueDiffOn` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `WithTop.add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Set` `Set.instMembership`	`ContinuousLinearMap` `RingHom.id` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContinuousLinearMap.toNormedSpace` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `fderivWithin`	—	`fderivWithin` `comp` `contDiffWithinAt_snd` `Set.prod_subset_preimage_snd` `contDiffWithinAt_id` `Set.preimage_id'` `subset_refl` `Set.instReflSubset`
`fderivWithin_right_apply` 📖	mathematical	`ContDiffWithinAt` `UniqueDiffOn` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `WithTop.add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Set` `Set.instMembership`	`DFunLike.coe` `ContinuousLinearMap` `RingHom.id` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.funLike` `fderivWithin`	—	`fderivWithin_apply` `comp` `contDiffWithinAt_snd` `Set.prod_subset_preimage_snd` `contDiffWithinAt_id` `Set.preimage_id'` `subset_refl` `Set.instReflSubset`
`hasFDerivWithinAt_nhds` 📖	mathematical	`ContDiffWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `WithTop` `ENat` `WithTop.add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `SProd.sprod` `Set` `Set.instSProd` `Set.instInsert` `Filter` `Filter.instMembership` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Set.image`	`Set.instHasSubset` `HasFDerivWithinAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContinuousLinearMap.toNormedSpace` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing`	—	`nhdsWithin_mono` `nhdsWithin_prod` `self_mem_nhdsWithin` `RingHomIsometric.ids` `smulCommClass_self` `contDiffWithinAt_succ_iff_hasFDerivWithinAt'` `Filter.inter_mem` `mem_of_mem_nhdsWithin` `Set.mem_insert` `mem_nhdsWithin_insert` `ContinuousWithinAt.preimage_mem_nhdsWithin'` `ContinuousWithinAt.prodMk` `continuousWithinAt_id` `continuousWithinAt` `nhdsWithin_le_iff` `LE.le.trans` `Set.subset_insert` `Set.inter_subset_right` `RingHomCompTriple.ids` `HasFDerivWithinAt.comp` `HasFDerivAt.hasFDerivWithinAt` `hasFDerivAt_prodMk_right` `Set.mapsTo_iff_image_subset` `Set.image_prodMk_subset_prod_right` `comp_of_mem_nhdsWithin_image` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsTopologicalAddGroup.toContinuousAdd` `Prod.smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `continuousLinearMap_comp` `prodMk` `contDiffWithinAt_id`
`iteratedFDerivWithin_right` 📖	mathematical	`ContDiffWithinAt` `UniqueDiffOn` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `WithTop.add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `AddMonoidWithOne.toNatCast` `WithTop.addMonoidWithOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Set` `Set.instMembership`	`ContinuousMultilinearMap` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousMultilinearMap.normedAddCommGroup'` `Fin.fintype` `ContinuousMultilinearMap.normedSpace'` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `AddCommGroup.toAddCommMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `iteratedFDerivWithin`	—	`smulCommClass_self` `continuousLinearMap_comp` `RingHomInvPair.ids` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `of_le` `CharP.cast_eq_zero` `CharP.ofCharZero` `WithTop.charZero` `add_zero` `RingHomIsometric.ids` `IsTopologicalAddGroup.toContinuousAdd` `ContinuousMultilinearMap.instSMulCommClass` `ContinuousMultilinearMap.instContinuousConstSMul` `fderivWithin_right` `add_assoc` `add_comm` `Nat.cast_succ` `le_rfl`
`smulRight` 📖	mathematical	`ContDiffWithinAt` `StrongDual` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `ContinuousLinearMap.toNormedAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedSpace` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomIsometric.ids` `ContinuousLinearMap.toNormedSpace` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `Algebra.to_smulCommClass` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id`	`ContinuousLinearMap` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `ContinuousLinearMap.smulRight` `Semiring.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IsBoundedSMul.continuousSMul` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `NormedSpace.toIsBoundedSMul`	—	`RingHomIsometric.ids` `Algebra.to_smulCommClass` `ContDiff.comp₂_contDiffWithinAt` `smulCommClass_self` `IsScalarTower.left` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `IsBoundedBilinearMap.contDiff` `isBoundedBilinearMap_smulRight`

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fderiv` 📖	mathematical	`ContDiff` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `Continuous` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	`ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `ContinuousLinearMap.topologicalSpace` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `fderiv`	—	`ContDiff.continuous` `RingHomIsometric.ids` `smulCommClass_self` `ContDiff.fderiv` `contDiff_zero`
`fderiv_one` 📖	mathematical	`ContDiff` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `WithTop` `ENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `Continuous` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	`ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `ContinuousLinearMap.topologicalSpace` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `fderiv`	—	`ContDiff.continuous` `RingHomIsometric.ids` `smulCommClass_self` `ContDiff.fderiv` `contDiff_zero` `le_refl`

ContinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousOn_iteratedFDeriv` 📖	mathematical	`ContDiffOn` `IsOpen` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `AddMonoidWithOne.toNatCast` `WithTop.addMonoidWithOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	`ContinuousOn` `ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousMultilinearMap.instTopologicalSpace` `NormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `iteratedFDeriv`	—	`ContinuousAt.continuousWithinAt` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContDiffAt.continuousAt_iteratedFDeriv` `ContDiffOn.contDiffAt` `IsOpen.mem_nhds`
`continuousOn_iteratedFDerivWithin` 📖	mathematical	`ContDiffOn` `UniqueDiffOn` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `AddMonoidWithOne.toNatCast` `WithTop.addMonoidWithOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	`ContinuousOn` `ContinuousMultilinearMap` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousMultilinearMap.instTopologicalSpace` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `iteratedFDerivWithin`	—	`ContDiffWithinAt.continuousWithinAt_iteratedFDerivWithin` `ContDiffOn.contDiffWithinAt`

Differentiable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fderiv_two` 📖	mathematical	`ContDiff` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `WithTop` `ENat` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `WithTop.addMonoidWithOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `Nat.instAtLeastTwoHAddOfNat` `WithTop.one` `AddMonoidWithOne.toOne`	`Differentiable` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContinuousLinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedSpace.toIsBoundedSMul` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.topologicalSpace` `fderiv`	—	`Nat.instAtLeastTwoHAddOfNat` `ContDiff.differentiable` `RingHomIsometric.ids` `smulCommClass_self` `contDiff_iff_contDiffAt` `ContDiffAt.fderiv` `ContDiff.contDiffAt` `le_refl` `one_ne_zero` `NeZero.charZero_one` `WithTop.charZero`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`contDiffAt_fst` 📖	mathematical	—	`ContDiffAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`ContDiff.contDiffAt` `contDiff_fst`
`contDiffAt_snd` 📖	mathematical	—	`ContDiffAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`ContDiff.contDiffAt` `contDiff_snd`
`contDiffOn_fderivWithin_apply` 📖	mathematical	`ContDiffOn` `UniqueDiffOn` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `WithTop.add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	`Prod.normedAddCommGroup` `Prod.normedSpace` `DFunLike.coe` `ContinuousLinearMap` `RingHom.id` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `ContinuousLinearMap.funLike` `fderivWithin` `SProd.sprod` `Set` `Set.instSProd` `Set.univ`	—	`ContDiffOn.clm_apply` `ContDiffOn.comp` `RingHomIsometric.ids` `smulCommClass_self` `ContDiffOn.fderivWithin` `contDiffOn_fst` `Set.prod_subset_preimage_fst` `contDiffOn_snd`
`contDiffOn_fst` 📖	mathematical	—	`ContDiffOn` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`ContDiff.contDiffOn` `contDiff_fst`
`contDiffOn_snd` 📖	mathematical	—	`ContDiffOn` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`ContDiff.contDiffOn` `contDiff_snd`
`contDiffWithinAt_fst` 📖	mathematical	—	`ContDiffWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`ContDiff.contDiffWithinAt` `contDiff_fst`
`contDiffWithinAt_snd` 📖	mathematical	—	`ContDiffWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`ContDiff.contDiffWithinAt` `contDiff_snd`
`contDiff_fst` 📖	mathematical	—	`ContDiff` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`IsBoundedLinearMap.contDiff` `IsBoundedLinearMap.fst`
`contDiff_snd` 📖	mathematical	—	`ContDiff` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`IsBoundedLinearMap.contDiff` `IsBoundedLinearMap.snd`
`iteratedFDerivWithin_clm_apply_const_apply` 📖	mathematical	`UniqueDiffOn` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ContDiffOn` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContinuousLinearMap.toNormedSpace` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `AddMonoidWithOne.toNatCast` `WithTop.addMonoidWithOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `CommSemiring.toSemiring` `instCommSemiringENat` `Set` `Set.instMembership`	`DFunLike.coe` `ContinuousMultilinearMap` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousMultilinearMap.funLike` `iteratedFDerivWithin` `ContinuousLinearMap.funLike`	—	`RingHomIsometric.ids` `smulCommClass_self` `lt_of_lt_of_le` `WithTop.addLeftMono` `IsOrderedAddMonoid.toAddLeftMono` `LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid` `WithTop.zeroLEOneClass` `IsOrderedRing.toZeroLEOneClass` `WithTop.charZero` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `Nat.instIsOrderedAddMonoid` `contravariant_lt_of_covariant_le` `Nat.instZeroLEOneClass` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `ContDiffOn.differentiableOn_iteratedFDerivWithin` `ContDiffOn.clm_apply` `contDiffOn_const` `ContinuousLinearMap.continuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `ContinuousLinearMap.smulCommClass` `ContinuousLinearMap.topologicalAddGroup` `fderivWithin_continuousMultilinear_apply_const_apply` `Finite.of_fintype` `fderivWithin_congr'` `LT.lt.le` `IsTopologicalAddGroup.toContinuousAdd` `RingHomCompTriple.ids` `fderivWithin_clm_apply` `DifferentiableOn.continuousMultilinear_apply_const` `differentiableWithinAt_const` `fderivWithin_const_apply` `ContinuousLinearMap.comp_zero` `zero_add`
`iteratedFDerivWithin_comp` 📖	mathematical	`ContDiffWithinAt` `UniqueDiffOn` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Set` `Set.instMembership` `Set.MapsTo` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `AddMonoidWithOne.toNatCast` `WithTop.addMonoidWithOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	`iteratedFDerivWithin` `FormalMultilinearSeries.taylorComp` `ftaylorSeriesWithin`	—	`iteratedFDerivWithin_comp_of_eventually_mem` `Filter.Eventually.mono` `eventually_mem_nhdsWithin`
`iteratedFDerivWithin_comp_of_eventually_mem` 📖	mathematical	`ContDiffWithinAt` `UniqueDiffOn` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Set` `Set.instMembership` `Filter.Eventually` `nhdsWithin` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `AddMonoidWithOne.toNatCast` `WithTop.addMonoidWithOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	`iteratedFDerivWithin` `FormalMultilinearSeries.taylorComp` `ftaylorSeriesWithin`	—	`Filter.Eventually.self_of_nhdsWithin` `tendsto_nhdsWithin_iff` `ContDiffWithinAt.continuousWithinAt` `ContDiffWithinAt.eventually_hasFTaylorSeriesUpToOn` `Filter.Tendsto.eventually` `Filter.Tendsto.image_smallSets` `Filter.HasBasis.eventually_iff` `Filter.HasBasis.smallSets` `nhdsWithin_basis_open` `Filter.Eventually.and` `Set.inter_comm` `Set.instReflSubset` `HasFTaylorSeriesUpToOn.eq_iteratedFDerivWithin_of_uniqueDiffOn` `HasFTaylorSeriesUpToOn.comp` `Set.mapsTo_image` `le_rfl` `UniqueDiffOn.inter` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `iteratedFDerivWithin_inter_open`
`iteratedFDeriv_clm_apply_const_apply` 📖	mathematical	`ContDiff` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContinuousLinearMap.toNormedSpace` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `AddMonoidWithOne.toNatCast` `WithTop.addMonoidWithOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `CommSemiring.toSemiring` `instCommSemiringENat`	`DFunLike.coe` `ContinuousMultilinearMap` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousMultilinearMap.funLike` `iteratedFDeriv` `ContinuousLinearMap.funLike`	—	`RingHomIsometric.ids` `smulCommClass_self` `iteratedFDerivWithin_clm_apply_const_apply` `uniqueDiffOn_univ` `NormedField.nhdsNE_neBot` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `ContDiff.contDiffOn` `Set.mem_univ`
`iteratedFDeriv_comp` 📖	mathematical	`ContDiffAt` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `AddMonoidWithOne.toNatCast` `WithTop.addMonoidWithOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	`iteratedFDeriv` `FormalMultilinearSeries.taylorComp` `ftaylorSeries`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `iteratedFDerivWithin_comp` `ContDiffAt.contDiffWithinAt` `uniqueDiffOn_univ` `NormedField.nhdsNE_neBot` `IsBoundedSMul.continuousSMul` `Set.mem_univ` `Set.mapsTo_univ`

---

← Back to Index