Basic

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

Statistics

Metric	Count
Definitions	0
Theorems `comp_continuousLinearMap`, `continuousLinearMap_comp`, `prodMk`, `continuousLinearMap_comp`, `prodMk`, `comp_continuousLinearMap`, `continuousLinearMap_comp`, `iUnion_of_isOpen`, `prodMk`, `union_of_isOpen`, `comp_continuousLinearMap`, `continuousLinearMap_comp`, `prodMk`, `comp_contDiffAt_iff`, `comp_contDiffOn_iff`, `comp_contDiffWithinAt_iff`, `comp_contDiff_iff`, `contDiff`, `contDiffAt_comp_iff`, `contDiffOn_comp_iff`, `contDiffWithinAt_comp_iff`, `contDiff_comp_iff`, `iteratedFDerivWithin_comp_left`, `iteratedFDerivWithin_comp_right`, `iteratedFDeriv_comp_left`, `contDiff`, `iteratedFDerivWithin_comp_left`, `iteratedFDerivWithin_comp_right`, `iteratedFDeriv_comp_left`, `iteratedFDeriv_comp_right`, `compContinuousLinearMap`, `comp_continuousAffineMap`, `continuousLinearMap_comp`, `prodMk`, `contDiff`, `contDiff`, `contDiff`, `norm_iteratedFDerivWithin_comp_left`, `norm_iteratedFDeriv_comp_left`, `contDiff`, `norm_iteratedFDerivWithin_comp_left`, `norm_iteratedFDerivWithin_comp_right`, `norm_iteratedFDeriv_comp_left`, `norm_iteratedFDeriv_comp_right`, `contDiffAt_const`, `contDiffAt_fun_id`, `contDiffAt_id`, `contDiffAt_of_subsingleton`, `contDiffOn_const`, `contDiffOn_fun_id`, `contDiffOn_iUnion_iff_of_isOpen`, `contDiffOn_id`, `contDiffOn_of_subsingleton`, `contDiffOn_union_iff_of_isOpen`, `contDiffWithinAt_const`, `contDiffWithinAt_fun_id`, `contDiffWithinAt_id`, `contDiffWithinAt_of_subsingleton`, `contDiffWithinAt_singleton`, `contDiff_const`, `contDiff_fun_id`, `contDiff_id`, `contDiff_of_contDiffOn_iUnion_of_isOpen`, `contDiff_of_contDiffOn_union_of_isOpen`, `contDiff_of_subsingleton`, `contDiff_prodAssoc`, `contDiff_prodAssoc_symm`, `contDiff_zero_fun`, `iteratedFDerivWithin_const_of_ne`, `iteratedFDerivWithin_prodMk`, `iteratedFDerivWithin_succ_const`, `iteratedFDerivWithin_zero_fun`, `iteratedFDeriv_const_of_ne`, `iteratedFDeriv_prodMk`, `iteratedFDeriv_succ_const`, `iteratedFDeriv_zero_fun`	76
Total	76

ContDiff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_continuousLinearMap` 📖	mathematical	`ContDiff`	`DFunLike.coe` `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.funLike`	—	`contDiffOn_univ` `ContDiffOn.comp_continuousLinearMap`
`continuousLinearMap_comp` 📖	mathematical	`ContDiff`	`DFunLike.coe` `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.funLike`	—	`contDiffOn_univ` `ContDiffOn.continuousLinearMap_comp`
`prodMk` 📖	mathematical	`ContDiff`	`Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`contDiffOn_univ` `ContDiffOn.prodMk` `contDiffOn`

ContDiffAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousLinearMap_comp` 📖	mathematical	`ContDiffAt`	`DFunLike.coe` `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.funLike`	—	`ContDiffWithinAt.continuousLinearMap_comp`
`prodMk` 📖	mathematical	`ContDiffAt`	`Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`contDiffWithinAt_univ` `ContDiffWithinAt.prodMk` `contDiffWithinAt`

ContDiffOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_continuousLinearMap` 📖	mathematical	`ContDiffOn`	`DFunLike.coe` `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.funLike` `Set.preimage`	—	`ContDiffWithinAt.comp_continuousLinearMap`
`continuousLinearMap_comp` 📖	mathematical	`ContDiffOn`	`DFunLike.coe` `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.funLike`	—	`ContDiffWithinAt.continuousLinearMap_comp`
`iUnion_of_isOpen` 📖	mathematical	`ContDiffOn` `IsOpen` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`Set.iUnion`	—	`ContDiffAt.contDiffWithinAt` `contDiffAt` `IsOpen.mem_nhds`
`prodMk` 📖	mathematical	`ContDiffOn`	`Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`ContDiffWithinAt.prodMk`
`union_of_isOpen` 📖	mathematical	`ContDiffOn` `IsOpen` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`Set` `Set.instUnion`	—	`ContDiffAt.contDiffWithinAt` `ContDiffWithinAt.contDiffAt` `IsOpen.mem_nhds`

ContDiffWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_continuousLinearMap` 📖	mathematical	`ContDiffWithinAt` `DFunLike.coe` `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.funLike`	`Set.preimage`	—	`ContinuousWithinAt.tendsto_nhdsWithin` `Continuous.continuousWithinAt` `ContinuousLinearMap.continuous` `Set.MapsTo.union_union` `Set.mapsTo_singleton` `Set.mem_singleton` `Set.mapsTo_preimage` `HasFTaylorSeriesUpToOn.compContinuousLinearMap` `AnalyticOn.comp` `smulCommClass_self` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsTopologicalAddGroup.toContinuousAdd` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `ContinuousLinearMap.analyticOn` `Set.mapsTo_univ`
`continuousLinearMap_comp` 📖	mathematical	`ContDiffWithinAt`	`DFunLike.coe` `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.funLike`	—	`HasFTaylorSeriesUpToOn.continuousLinearMap_comp` `AnalyticOnNhd.comp_analyticOn` `smulCommClass_self` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsTopologicalAddGroup.toContinuousAdd` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `ContinuousMultilinearMap.instIsTopologicalAddGroup` `ContinuousMultilinearMap.instSMulCommClass` `ContinuousMultilinearMap.instContinuousConstSMul` `ContinuousLinearMap.analyticOnNhd` `Set.mapsTo_univ`
`prodMk` 📖	mathematical	`ContDiffWithinAt`	`Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`Filter.inter_mem` `HasFTaylorSeriesUpToOn.prodMk` `HasFTaylorSeriesUpToOn.mono` `Set.inter_subset_left` `Set.inter_subset_right` `AnalyticOnNhd.comp_analyticOn` `smulCommClass_self` `Prod.smulCommClass` `RingHomInvPair.ids` `LinearIsometryEquiv.analyticOnNhd` `AnalyticOn.prod` `AnalyticOn.mono` `Set.mapsTo_univ`

ContinuousLinearEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_contDiffAt_iff` 📖	mathematical	—	`ContDiffAt` `DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `EquivLike.toFunLike` `equivLike`	—	`RingHomInvPair.ids` `comp_contDiffWithinAt_iff`
`comp_contDiffOn_iff` 📖	mathematical	—	`ContDiffOn` `DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `EquivLike.toFunLike` `equivLike`	—	`RingHomInvPair.ids` `comp_contDiffWithinAt_iff`
`comp_contDiffWithinAt_iff` 📖	mathematical	—	`ContDiffWithinAt` `DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `EquivLike.toFunLike` `equivLike`	—	`RingHomInvPair.ids` `symm_apply_apply` `ContDiffWithinAt.continuousLinearMap_comp`
`comp_contDiff_iff` 📖	mathematical	—	`ContDiff` `DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `EquivLike.toFunLike` `equivLike`	—	`RingHomInvPair.ids` `comp_contDiffOn_iff`
`contDiff` 📖	mathematical	—	`ContDiff` `DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `EquivLike.toFunLike` `equivLike`	—	`RingHomInvPair.ids` `ContinuousLinearMap.contDiff`
`contDiffAt_comp_iff` 📖	mathematical	—	`ContDiffAt` `DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `EquivLike.toFunLike` `equivLike` `symm`	—	`RingHomInvPair.ids` `contDiffWithinAt_univ` `Set.preimage_univ` `contDiffWithinAt_comp_iff`
`contDiffOn_comp_iff` 📖	mathematical	—	`ContDiffOn` `DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `EquivLike.toFunLike` `equivLike` `Set.preimage`	—	`RingHomInvPair.ids` `apply_symm_apply` `symm_preimage_preimage` `ContDiffOn.comp_continuousLinearMap`
`contDiffWithinAt_comp_iff` 📖	mathematical	—	`ContDiffWithinAt` `DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `EquivLike.toFunLike` `equivLike` `Set.preimage` `symm`	—	`RingHomInvPair.ids` `apply_symm_apply` `ContDiffWithinAt.comp_continuousLinearMap` `coe_coe`
`contDiff_comp_iff` 📖	mathematical	—	`ContDiff` `DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `EquivLike.toFunLike` `equivLike`	—	`RingHomInvPair.ids` `contDiffOn_univ` `Set.preimage_univ` `contDiffOn_comp_iff`
`iteratedFDerivWithin_comp_left` 📖	mathematical	`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`	`iteratedFDerivWithin` `DFunLike.coe` `ContinuousLinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `EquivLike.toFunLike` `equivLike` `ContinuousLinearMap.compContinuousMultilinearMap` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `toContinuousLinearMap`	—	`RingHomInvPair.ids` `ContinuousMultilinearMap.ext` `ContinuousLinearMap.compContinuousMultilinearMap_coe` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `smulCommClass_self` `iteratedFDerivWithin_succ_apply_left` `IsTopologicalAddGroup.toContinuousAdd` `fderivWithin_congr'` `RingHomCompTriple.ids` `comp_fderivWithin` `EquivLike.toEmbeddingLike`
`iteratedFDerivWithin_comp_right` 📖	mathematical	`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` `DFunLike.coe` `ContinuousLinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `EquivLike.toFunLike` `equivLike`	`iteratedFDerivWithin` `Set.preimage` `ContinuousMultilinearMap.compContinuousLinearMap` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `toContinuousLinearMap`	—	`RingHomInvPair.ids` `ContinuousMultilinearMap.ext` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `smulCommClass_self` `IsTopologicalAddGroup.toContinuousAdd` `fderivWithin_congr'` `RingHomCompTriple.ids` `comp_fderivWithin` `uniqueDiffOn_preimage_iff` `comp_right_fderivWithin` `ContinuousLinearMap.coe_comp'` `coe_coe` `Fin.tail_def`
`iteratedFDeriv_comp_left` 📖	mathematical	—	`iteratedFDeriv` `DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `EquivLike.toFunLike` `equivLike` `ContinuousLinearMap.compContinuousMultilinearMap` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `toContinuousLinearMap`	—	`RingHomInvPair.ids` `iteratedFDerivWithin_comp_left` `uniqueDiffOn_univ` `NormedField.nhdsNE_neBot` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul`

ContinuousLinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`contDiff` 📖	mathematical	—	`ContDiff` `DFunLike.coe` `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` `funLike`	—	`IsBoundedLinearMap.contDiff` `isBoundedLinearMap`
`iteratedFDerivWithin_comp_left` 📖	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` `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` `DFunLike.coe` `ContinuousLinearMap` `RingHom.id` `AddCommGroup.toAddCommMonoid` `funLike` `compContinuousMultilinearMap` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`ContDiffWithinAt.contDiffOn'` `instIsEmptyFalse` `iteratedFDerivWithin_inter_open` `HasFTaylorSeriesUpToOn.eq_iteratedFDerivWithin_of_uniqueDiffOn` `HasFTaylorSeriesUpToOn.continuousLinearMap_comp` `ContDiffOn.ftaylorSeriesWithin` `Set.insert_eq_of_mem` `UniqueDiffOn.inter` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `le_rfl`
`iteratedFDerivWithin_comp_right` 📖	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` `Set.preimage` `DFunLike.coe` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `funLike` `Set` `Set.instMembership` `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`	`iteratedFDerivWithin` `ContinuousMultilinearMap.compContinuousLinearMap` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`HasFTaylorSeriesUpToOn.eq_iteratedFDerivWithin_of_uniqueDiffOn` `HasFTaylorSeriesUpToOn.compContinuousLinearMap` `ContDiffOn.ftaylorSeriesWithin` `ContDiffOn.of_le` `le_rfl`
`iteratedFDeriv_comp_left` 📖	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` `DFunLike.coe` `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` `funLike` `compContinuousMultilinearMap` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`iteratedFDerivWithin_comp_left` `ContDiffAt.contDiffWithinAt` `uniqueDiffOn_univ` `NormedField.nhdsNE_neBot` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `Set.mem_univ`
`iteratedFDeriv_comp_right` 📖	mathematical	`ContDiff` `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` `DFunLike.coe` `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` `funLike` `ContinuousMultilinearMap.compContinuousLinearMap` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`iteratedFDerivWithin_comp_right` `ContDiff.contDiffOn` `uniqueDiffOn_univ` `NormedField.nhdsNE_neBot` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `Set.mem_univ`

HasFTaylorSeriesUpToOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compContinuousLinearMap` 📖	mathematical	`HasFTaylorSeriesUpToOn`	`DFunLike.coe` `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.funLike` `ContinuousMultilinearMap.compContinuousLinearMap` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Set.preimage`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `comp_continuousAffineMap`
`comp_continuousAffineMap` 📖	mathematical	`HasFTaylorSeriesUpToOn`	`DFunLike.coe` `ContinuousAffineMap` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddTorsor.toAddTorsor` `SeminormedAddCommGroup.toNormedAddTorsor` `ContinuousAffineMap.instFunLike` `ContinuousMultilinearMap.compContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `AddCommGroup.toAddCommMonoid` `ContinuousAffineMap.contLinear` `instIsTopologicalAddTorsor_1` `Set.preimage`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `instIsTopologicalAddTorsor_1` `smulCommClass_self` `isBoundedLinearMap_continuousMultilinearMap_comp_linear` `zero_eq` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass` `RingHomCompTriple.ids` `ContinuousLinearMap.ext` `ContinuousMultilinearMap.ext` `Fin.comp_cons` `HasFDerivAt.comp_hasFDerivWithinAt` `IsBoundedLinearMap.hasFDerivAt` `HasFDerivWithinAt.comp` `fderivWithin` `ContinuousAffineMap.hasFDerivWithinAt` `Set.Subset.refl` `Continuous.comp_continuousOn` `IsBoundedLinearMap.continuous` `ContinuousOn.comp` `cont` `Continuous.continuousOn` `ContinuousAffineMap.continuous`
`continuousLinearMap_comp` 📖	mathematical	`HasFTaylorSeriesUpToOn`	`DFunLike.coe` `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.funLike` `ContinuousLinearMap.compContinuousMultilinearMap` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `zero_eq` `HasFDerivAt.comp_hasFDerivWithinAt` `smulCommClass_self` `ContinuousMultilinearMap.instIsTopologicalAddGroup` `ContinuousMultilinearMap.instSMulCommClass` `ContinuousMultilinearMap.instContinuousConstSMul` `ContinuousLinearMap.hasFDerivAt` `fderivWithin` `Continuous.comp_continuousOn` `ContinuousLinearMap.continuous` `cont`
`prodMk` 📖	mathematical	`HasFTaylorSeriesUpToOn`	`Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ContinuousMultilinearMap.prod` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `PseudoEMetricSpace.toUniformSpace` `PseudoMetricSpace.toPseudoEMetricSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `RingHomInvPair.ids` `smulCommClass_self` `Prod.continuousConstSMul` `Prod.smulCommClass` `zero_eq` `RingHomCompTriple.ids` `HasFDerivAt.comp_hasFDerivWithinAt` `LinearIsometryEquiv.hasFDerivAt` `HasFDerivWithinAt.prodMk` `fderivWithin` `Continuous.comp_continuousOn` `LinearIsometryEquiv.continuous` `ContinuousOn.prodMk` `cont`

IsBoundedBilinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`contDiff` 📖	mathematical	`IsBoundedBilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule`	`ContDiff` `Prod.normedAddCommGroup` `Prod.normedSpace`	—	`AnalyticOnNhd.contDiff` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsTopologicalAddGroup.toContinuousAdd` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `ContinuousLinearMap.analyticOnNhd_bilinear`

IsBoundedLinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`contDiff` 📖	mathematical	`IsBoundedLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule`	`ContDiff`	—	`AnalyticOnNhd.contDiff` `ContinuousLinearMap.analyticOnNhd`

LinearIsometry

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`contDiff` 📖	mathematical	—	`ContDiff` `DFunLike.coe` `LinearIsometry` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `instFunLike`	—	`ContinuousLinearMap.contDiff`
`norm_iteratedFDerivWithin_comp_left` 📖	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` `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`	`Norm.norm` `ContinuousMultilinearMap` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousMultilinearMap.hasOpNorm'` `Fin.fintype` `iteratedFDerivWithin` `DFunLike.coe` `LinearIsometry` `RingHom.id` `instFunLike`	—	`ContinuousLinearMap.iteratedFDerivWithin_comp_left` `norm_compContinuousMultilinearMap`
`norm_iteratedFDeriv_comp_left` 📖	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`	`Norm.norm` `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.hasOpNorm'` `Fin.fintype` `iteratedFDeriv` `DFunLike.coe` `LinearIsometry` `RingHom.id` `instFunLike`	—	`norm_iteratedFDerivWithin_comp_left` `ContDiffAt.contDiffWithinAt` `uniqueDiffOn_univ` `NormedField.nhdsNE_neBot` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `Set.mem_univ`

LinearIsometryEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`contDiff` 📖	mathematical	—	`ContDiff` `DFunLike.coe` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `EquivLike.toFunLike` `instEquivLike`	—	`RingHomInvPair.ids` `ContinuousLinearMap.contDiff`
`norm_iteratedFDerivWithin_comp_left` 📖	mathematical	`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`	`Norm.norm` `ContinuousMultilinearMap` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousMultilinearMap.hasOpNorm'` `Fin.fintype` `iteratedFDerivWithin` `DFunLike.coe` `LinearIsometryEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EquivLike.toFunLike` `instEquivLike`	—	`RingHomInvPair.ids` `ContinuousLinearEquiv.iteratedFDerivWithin_comp_left` `LinearIsometry.norm_compContinuousMultilinearMap`
`norm_iteratedFDerivWithin_comp_right` 📖	mathematical	`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` `DFunLike.coe` `LinearIsometryEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EquivLike.toFunLike` `instEquivLike`	`Norm.norm` `ContinuousMultilinearMap` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousMultilinearMap.hasOpNorm'` `Fin.fintype` `iteratedFDerivWithin` `Set.preimage`	—	`RingHomInvPair.ids` `ContinuousLinearEquiv.iteratedFDerivWithin_comp_right` `ContinuousMultilinearMap.norm_compContinuous_linearIsometryEquiv`
`norm_iteratedFDeriv_comp_left` 📖	mathematical	—	`Norm.norm` `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.hasOpNorm'` `Fin.fintype` `iteratedFDeriv` `DFunLike.coe` `LinearIsometryEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EquivLike.toFunLike` `instEquivLike`	—	`RingHomInvPair.ids` `iteratedFDerivWithin_univ` `norm_iteratedFDerivWithin_comp_left` `uniqueDiffOn_univ` `NormedField.nhdsNE_neBot` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `Set.mem_univ`
`norm_iteratedFDeriv_comp_right` 📖	mathematical	—	`Norm.norm` `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.hasOpNorm'` `Fin.fintype` `iteratedFDeriv` `DFunLike.coe` `LinearIsometryEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EquivLike.toFunLike` `instEquivLike`	—	`RingHomInvPair.ids` `norm_iteratedFDerivWithin_comp_right` `uniqueDiffOn_univ` `NormedField.nhdsNE_neBot` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `Set.mem_univ`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`contDiffAt_const` 📖	mathematical	—	`ContDiffAt`	—	`ContDiff.contDiffAt` `contDiff_const`
`contDiffAt_fun_id` 📖	mathematical	—	`ContDiffAt`	—	`ContDiff.contDiffAt` `contDiff_id`
`contDiffAt_id` 📖	mathematical	—	`ContDiffAt`	—	`ContDiff.contDiffAt` `contDiff_id`
`contDiffAt_of_subsingleton` 📖	mathematical	—	`ContDiffAt`	—	`contDiffAt_const`
`contDiffOn_const` 📖	mathematical	—	`ContDiffOn`	—	`ContDiff.contDiffOn` `contDiff_const`
`contDiffOn_fun_id` 📖	mathematical	—	`ContDiffOn`	—	`ContDiff.contDiffOn` `contDiff_id`
`contDiffOn_iUnion_iff_of_isOpen` 📖	mathematical	`IsOpen` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`ContDiffOn` `Set.iUnion`	—	`ContDiffOn.mono` `Set.subset_iUnion_of_subset` `ContDiffOn.iUnion_of_isOpen`
`contDiffOn_id` 📖	mathematical	—	`ContDiffOn`	—	`ContDiff.contDiffOn` `contDiff_id`
`contDiffOn_of_subsingleton` 📖	mathematical	—	`ContDiffOn`	—	`contDiffOn_const`
`contDiffOn_union_iff_of_isOpen` 📖	mathematical	`IsOpen` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`ContDiffOn` `Set` `Set.instUnion`	—	`ContDiffOn.mono` `Set.subset_union_left` `Set.subset_union_right` `ContDiffOn.union_of_isOpen`
`contDiffWithinAt_const` 📖	mathematical	—	`ContDiffWithinAt`	—	`ContDiffAt.contDiffWithinAt` `contDiffAt_const`
`contDiffWithinAt_fun_id` 📖	mathematical	—	`ContDiffWithinAt`	—	`ContDiff.contDiffWithinAt` `contDiff_id`
`contDiffWithinAt_id` 📖	mathematical	—	`ContDiffWithinAt`	—	`ContDiff.contDiffWithinAt` `contDiff_id`
`contDiffWithinAt_of_subsingleton` 📖	mathematical	—	`ContDiffWithinAt`	—	`contDiffWithinAt_const`
`contDiffWithinAt_singleton` 📖	mathematical	—	`ContDiffWithinAt` `Set` `Set.instSingletonSet`	—	`ContDiffWithinAt.congr` `contDiffWithinAt_const`
`contDiff_const` 📖	mathematical	—	`ContDiff`	—	`AnalyticOnNhd.contDiff` `analyticOnNhd_const`
`contDiff_fun_id` 📖	mathematical	—	`ContDiff`	—	`IsBoundedLinearMap.contDiff` `IsBoundedLinearMap.id`
`contDiff_id` 📖	mathematical	—	`ContDiff`	—	`IsBoundedLinearMap.contDiff` `IsBoundedLinearMap.id`
`contDiff_of_contDiffOn_iUnion_of_isOpen` 📖	mathematical	`ContDiffOn` `IsOpen` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set.iUnion` `Set.univ`	`ContDiff`	—	`contDiffOn_univ` `ContDiffOn.iUnion_of_isOpen`
`contDiff_of_contDiffOn_union_of_isOpen` 📖	mathematical	`ContDiffOn` `Set` `Set.instUnion` `Set.univ` `IsOpen` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`ContDiff`	—	`contDiffOn_univ` `ContDiffOn.union_of_isOpen`
`contDiff_of_subsingleton` 📖	mathematical	—	`ContDiff`	—	`contDiff_const`
`contDiff_prodAssoc` 📖	mathematical	—	`ContDiff` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.prodAssoc`	—	`LinearIsometryEquiv.contDiff`
`contDiff_prodAssoc_symm` 📖	mathematical	—	`ContDiff` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `Equiv.prodAssoc`	—	`LinearIsometryEquiv.contDiff` `RingHomInvPair.ids`
`contDiff_zero_fun` 📖	mathematical	—	`ContDiff` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`AnalyticOnNhd.contDiff` `analyticOnNhd_const`
`iteratedFDerivWithin_const_of_ne` 📖	mathematical	—	`iteratedFDerivWithin` `Pi.instZero` `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.instZero`	—	`iteratedFDerivWithin_succ_const`
`iteratedFDerivWithin_prodMk` 📖	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` `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` `Prod.normedAddCommGroup` `Prod.normedSpace` `ContinuousMultilinearMap.prod` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`ContinuousMultilinearMap.prod_ext` `ContinuousMultilinearMap.ext` `ContinuousLinearMap.iteratedFDerivWithin_comp_left` `ContDiffWithinAt.prodMk` `ContinuousLinearMap.compContinuousMultilinearMap_coe`
`iteratedFDerivWithin_succ_const` 📖	mathematical	—	`iteratedFDerivWithin` `Pi.instZero` `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.instZero`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsTopologicalAddGroup.toContinuousAdd` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `smulCommClass_self` `RingHomInvPair.ids` `RingHomIsometric.ids` `ContinuousMultilinearMap.instSMulCommClass` `ContinuousMultilinearMap.instContinuousConstSMul` `fderivWithin_fun_const` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearIsometryClass.toSemilinearMapClass` `SemilinearIsometryEquivClass.toSemilinearIsometryClass` `LinearIsometryEquiv.instSemilinearIsometryEquivClass` `iteratedFDerivWithin_succ_eq_comp_left`
`iteratedFDerivWithin_zero_fun` 📖	mathematical	—	`iteratedFDerivWithin` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Pi.instZero` `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.instZero`	—	`ContinuousMultilinearMap.ext` `iteratedFDerivWithin_succ_const`
`iteratedFDeriv_const_of_ne` 📖	mathematical	—	`iteratedFDeriv` `Pi.instZero` `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.instZero`	—	`iteratedFDerivWithin_const_of_ne`
`iteratedFDeriv_prodMk` 📖	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` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ContinuousMultilinearMap.prod` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule`	—	`iteratedFDerivWithin_prodMk` `ContDiffAt.contDiffWithinAt` `uniqueDiffOn_univ` `NormedField.nhdsNE_neBot` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `Set.mem_univ`
`iteratedFDeriv_succ_const` 📖	mathematical	—	`iteratedFDeriv` `Pi.instZero` `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.instZero`	—	`iteratedFDeriv_const_of_ne`
`iteratedFDeriv_zero_fun` 📖	mathematical	—	`iteratedFDeriv` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Pi.instZero` `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.instZero`	—	`iteratedFDerivWithin_zero_fun`

---

← Back to Index