Basic

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

Statistics

Metric	Count
Definitions `extDeriv`, `extDerivWithin`	2
Theorems `extDeriv`, `extDerivWithin`, `extDerivWithin'`, `extDerivWithin_eq`, `extDerivWithin_eq_nhds`, `extDerivWithin_eq_of_insert`, `extDerivWithin_eq_of_mem`, `extDeriv_eq`, `extDerivWithin_add`, `extDerivWithin_apply`, `extDerivWithin_congr`, `extDerivWithin_congr'`, `extDerivWithin_constOfIsEmpty`, `extDerivWithin_extDerivWithin_apply`, `extDerivWithin_extDerivWithin_eqOn`, `extDerivWithin_fun_add`, `extDerivWithin_fun_smul`, `extDerivWithin_pullback`, `extDerivWithin_smul`, `extDerivWithin_univ`, `extDeriv_add`, `extDeriv_apply`, `extDeriv_constOfIsEmpty`, `extDeriv_extDeriv`, `extDeriv_extDeriv_apply`, `extDeriv_fun_add`, `extDeriv_fun_smul`, `extDeriv_pullback`, `extDeriv_smul`	29
Total	31

Filter.EventuallyEq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`extDeriv` 📖	mathematical	`Filter.EventuallyEq` `ContinuousAlternatingMap` `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` `nhds`	`extDeriv`	—	`extDerivWithin`
`extDerivWithin` 📖	mathematical	`Filter.EventuallyEq` `ContinuousAlternatingMap` `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` `nhdsWithin`	`extDerivWithin`	—	`extDerivWithin'` `Set.Subset.rfl`
`extDerivWithin'` 📖	mathematical	`Filter.EventuallyEq` `ContinuousAlternatingMap` `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` `nhdsWithin` `Set` `Set.instHasSubset`	`extDerivWithin`	—	`Filter.Eventually.mp` `eventually_eventually_nhdsWithin` `Filter.Eventually.mono` `eventually_mem_nhdsWithin` `extDerivWithin_eq` `Filter.Eventually.filter_mono` `nhdsWithin_mono` `Filter.Eventually.self_of_nhdsWithin`
`extDerivWithin_eq` 📖	mathematical	`Filter.EventuallyEq` `ContinuousAlternatingMap` `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` `nhdsWithin`	`extDerivWithin`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `fderivWithin_eq`
`extDerivWithin_eq_nhds` 📖	mathematical	`Filter.EventuallyEq` `ContinuousAlternatingMap` `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` `nhds`	`extDerivWithin`	—	`extDerivWithin_eq` `filter_mono` `nhdsWithin_le_nhds` `Filter.Eventually.self_of_nhds`
`extDerivWithin_eq_of_insert` 📖	mathematical	`Filter.EventuallyEq` `ContinuousAlternatingMap` `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` `nhdsWithin` `Set` `Set.instInsert`	`extDerivWithin`	—	`extDerivWithin_eq` `nhdsWithin_mono` `Set.subset_insert` `mem_of_mem_nhdsWithin` `Set.mem_insert`
`extDerivWithin_eq_of_mem` 📖	mathematical	`Filter.EventuallyEq` `ContinuousAlternatingMap` `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` `nhdsWithin` `Set` `Set.instMembership`	`extDerivWithin`	—	`extDerivWithin_eq` `mem_of_mem_nhdsWithin`
`extDeriv_eq` 📖	mathematical	`Filter.EventuallyEq` `ContinuousAlternatingMap` `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` `nhds`	`extDeriv`	—	`Filter.Eventually.self_of_nhds` `extDeriv`

(root)

Definitions

Name	Category	Theorems
`extDeriv` 📖	CompOp	14 math math: `extDeriv_constOfIsEmpty`, `extDeriv_fun_smul`, `extDeriv_apply_vectorField`, `extDeriv_extDeriv`, `extDeriv_smul`, `extDerivWithin_univ`, `extDeriv_add`, `Filter.EventuallyEq.extDeriv`, `extDeriv_fun_add`, `Filter.EventuallyEq.extDeriv_eq`, `extDeriv_apply_vectorField_of_pairwise_commute`, `extDeriv_extDeriv_apply`, `extDeriv_pullback`, `extDeriv_apply`
`extDerivWithin` 📖	CompOp	20 math math: `extDerivWithin_congr`, `extDerivWithin_fun_add`, `extDerivWithin_pullback`, `extDerivWithin_constOfIsEmpty`, `extDerivWithin_add`, `Filter.EventuallyEq.extDerivWithin_eq_of_insert`, `extDerivWithin_extDerivWithin_eqOn`, `extDerivWithin_apply_vectorField_of_pairwise_commute`, `extDerivWithin_fun_smul`, `Filter.EventuallyEq.extDerivWithin_eq_of_mem`, `Filter.EventuallyEq.extDerivWithin'`, `extDerivWithin_univ`, `extDerivWithin_apply_vectorField`, `extDerivWithin_congr'`, `Filter.EventuallyEq.extDerivWithin_eq`, `Filter.EventuallyEq.extDerivWithin`, `extDerivWithin_extDerivWithin_apply`, `extDerivWithin_smul`, `extDerivWithin_apply`, `Filter.EventuallyEq.extDerivWithin_eq_nhds`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`extDerivWithin_add` 📖	mathematical	`UniqueDiffWithinAt` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DifferentiableWithinAt` `ContinuousAlternatingMap` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousAlternatingMap.instAddCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousAlternatingMap.instModule` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `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` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `Ring.toSemiring` `CommRing.toRing` `ContinuousAlternatingMap.instTopologicalSpace`	`extDerivWithin` `Pi.instAdd` `ContinuousAlternatingMap.instAdd` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `smulCommClass_self` `IsTopologicalAddGroup.toContinuousAdd` `fderivWithin_add` `ContinuousAlternatingMap.alternatizeUncurryFin_add`
`extDerivWithin_apply` 📖	mathematical	`DifferentiableWithinAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ContinuousAlternatingMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousAlternatingMap.instAddCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousAlternatingMap.instModule` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `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` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `Ring.toSemiring` `CommRing.toRing` `ContinuousAlternatingMap.instTopologicalSpace` `UniqueDiffWithinAt`	`DFunLike.coe` `ContinuousAlternatingMap.funLike` `extDerivWithin` `Finset.sum` `Finset.univ` `Fin.fintype` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `Monoid.toNatPow` `Int.instMonoid` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.funLike` `fderivWithin` `Fin.removeNth`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `smulCommClass_self` `IsTopologicalAddGroup.toContinuousAdd` `ContinuousAlternatingMap.alternatizeUncurryFin_apply` `Finset.sum_congr` `fderivWithin_continuousAlternatingMap_apply_const_apply` `Finite.of_fintype`
`extDerivWithin_congr` 📖	mathematical	`Set.EqOn` `ContinuousAlternatingMap` `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`	`extDerivWithin`	—	`Filter.EventuallyEq.extDerivWithin_eq` `Filter.EventuallyEq.filter_mono` `Set.EqOn.eventuallyEq` `inf_le_right`
`extDerivWithin_congr'` 📖	mathematical	`Set.EqOn` `ContinuousAlternatingMap` `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` `Set` `Set.instMembership`	`extDerivWithin`	—	`extDerivWithin_congr`
`extDerivWithin_constOfIsEmpty` 📖	mathematical	`UniqueDiffWithinAt` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	`extDerivWithin` `ContinuousAlternatingMap.constOfIsEmpty` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Fin.isEmpty'` `DFunLike.coe` `Equiv` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `ContinuousAlternatingMap` `EquivLike.toFunLike` `Equiv.instEquivLike` `ContinuousAlternatingMap.ofSubsingleton` `fderivWithin` `SeminormedAddCommGroup.toAddCommGroup`	—	`Fin.isEmpty'` `smulCommClass_self` `RingHomCompTriple.ids` `RingHomInvPair.ids` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `LinearIsometryEquiv.comp_fderivWithin` `ContinuousAlternatingMap.alternatizeUncurryFin_constOfIsEmptyLIE_comp`
`extDerivWithin_extDerivWithin_apply` 📖	mathematical	`ContDiffWithinAt` `ContinuousAlternatingMap` `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` `ContinuousAlternatingMap.instNormedAddCommGroup` `Fin.fintype` `ContinuousAlternatingMap.instNormedSpace` `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` `minSmoothness` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `WithTop.addMonoidWithOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `Nat.instAtLeastTwoHAddOfNat` `UniqueDiffOn` `NormedAddCommGroup.toAddCommGroup` `Set` `Set.instMembership` `closure` `interior`	`extDerivWithin` `ContinuousAlternatingMap.instZero`	—	`smulCommClass_self` `Nat.instAtLeastTwoHAddOfNat` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsTopologicalAddGroup.toContinuousAdd` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `ContinuousAlternatingMap.instIsTopologicalAddGroup` `ContinuousAlternatingMap.instSMulCommClass` `ContinuousAlternatingMap.instContinuousConstSMul` `RingHomCompTriple.ids` `ContDiffWithinAt.differentiableWithinAt` `RingHomIsometric.ids` `ContDiffWithinAt.fderivWithin_right` `LE.le.trans` `le_minSmoothness` `one_ne_zero` `NeZero.charZero_one` `WithTop.charZero` `HasFDerivWithinAt.fderivWithin` `IsBoundedSMul.continuousSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `ContinuousAlternatingMap.instContinuousSMul` `ContinuousAlternatingMap.instT2Space` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `HasFDerivAt.comp_hasFDerivWithinAt` `ContinuousLinearMap.hasFDerivAt` `DifferentiableWithinAt.hasFDerivWithinAt` `UniqueDiffOn.uniqueDiffWithinAt` `ContinuousAlternatingMap.alternatizeUncurryFin_alternatizeUncurryFinCLM_comp_of_symmetric` `ContDiffWithinAt.isSymmSndFDerivWithinAt`
`extDerivWithin_extDerivWithin_eqOn` 📖	mathematical	`ContDiffOn` `ContinuousAlternatingMap` `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` `ContinuousAlternatingMap.instNormedAddCommGroup` `Fin.fintype` `ContinuousAlternatingMap.instNormedSpace` `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` `minSmoothness` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `WithTop.addMonoidWithOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `Nat.instAtLeastTwoHAddOfNat` `UniqueDiffOn` `NormedAddCommGroup.toAddCommGroup`	`Set.EqOn` `extDerivWithin` `Pi.instZero` `ContinuousAlternatingMap.instZero` `Set` `Set.instInter` `closure` `interior`	—	`smulCommClass_self` `Nat.instAtLeastTwoHAddOfNat` `extDerivWithin_extDerivWithin_apply` `ContDiffOn.contDiffWithinAt`
`extDerivWithin_fun_add` 📖	mathematical	`UniqueDiffWithinAt` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DifferentiableWithinAt` `ContinuousAlternatingMap` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousAlternatingMap.instAddCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousAlternatingMap.instModule` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `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` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `Ring.toSemiring` `CommRing.toRing` `ContinuousAlternatingMap.instTopologicalSpace`	`extDerivWithin` `ContinuousAlternatingMap.instAdd` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `smulCommClass_self` `extDerivWithin_add`
`extDerivWithin_fun_smul` 📖	mathematical	`UniqueDiffWithinAt` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	`extDerivWithin` `ContinuousAlternatingMap` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousAlternatingMap.instSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `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` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `Ring.toSemiring` `CommRing.toRing`	—	`extDerivWithin_smul`
`extDerivWithin_pullback` 📖	mathematical	`DifferentiableWithinAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ContinuousAlternatingMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousAlternatingMap.instAddCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousAlternatingMap.instModule` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `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` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `Ring.toSemiring` `CommRing.toRing` `ContinuousAlternatingMap.instTopologicalSpace` `ContDiffWithinAt` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `minSmoothness` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `WithTop.addMonoidWithOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `Nat.instAtLeastTwoHAddOfNat` `UniqueDiffOn` `Set` `Set.instMembership` `closure` `interior` `Set.MapsTo`	`extDerivWithin` `ContinuousAlternatingMap.compContinuousLinearMap` `fderivWithin` `AddCommGroup.toAddCommMonoid`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `smulCommClass_self` `Nat.instAtLeastTwoHAddOfNat` `ContDiffWithinAt.differentiableWithinAt` `LT.lt.ne'` `LT.lt.trans_le` `two_pos` `WithTop.zeroLEOneClass` `IsOrderedRing.toZeroLEOneClass` `NeZero.charZero_one` `WithTop.charZero` `WithTop.addLeftMono` `IsOrderedAddMonoid.toAddLeftMono` `LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid` `LE.le.trans` `le_minSmoothness` `RingHomIsometric.ids` `ContDiffWithinAt.fderivWithin_right` `one_ne_zero` `extDerivWithin.eq_1` `IsTopologicalAddGroup.toContinuousAdd` `ContinuousAlternatingMap.instIsTopologicalAddGroup` `RingHomCompTriple.ids` `fderivWithin_continuousAlternatingMapCompContinuousLinearMap` `DifferentiableWithinAt.comp` `ContinuousAlternatingMap.alternatizeUncurryFin_add` `fderivWithin_comp'` `ContinuousAlternatingMap.alternatizeUncurryFin_fderivCompContinuousLinearMap_eq_zero` `ContDiffWithinAt.isSymmSndFDerivWithinAt` `add_zero` `ContinuousAlternatingMap.ext` `ContinuousAlternatingMap.alternatizeUncurryFin_apply` `Finset.sum_congr`
`extDerivWithin_smul` 📖	mathematical	`UniqueDiffWithinAt` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	`extDerivWithin` `Function.hasSMul` `ContinuousAlternatingMap` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousAlternatingMap.instSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `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` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `Ring.toSemiring` `CommRing.toRing`	—	`UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `smulCommClass_self` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousAlternatingMap.instSMulCommClass` `ContinuousAlternatingMap.instContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `fderivWithin_const_smul_field` `ContinuousAlternatingMap.alternatizeUncurryFin_smul`
`extDerivWithin_univ` 📖	mathematical	—	`extDerivWithin` `Set.univ` `extDeriv`	—	`extDerivWithin.eq_1` `extDeriv.eq_1` `fderivWithin_univ`
`extDeriv_add` 📖	mathematical	`DifferentiableAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ContinuousAlternatingMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousAlternatingMap.instAddCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousAlternatingMap.instModule` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `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` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `Ring.toSemiring` `CommRing.toRing` `ContinuousAlternatingMap.instTopologicalSpace`	`extDeriv` `Pi.instAdd` `ContinuousAlternatingMap.instAdd` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `smulCommClass_self` `IsTopologicalAddGroup.toContinuousAdd` `extDerivWithin_add` `PerfectSpace.not_isolated` `instPerfectSpace` `IsBoundedSMul.continuousSMul`
`extDeriv_apply` 📖	mathematical	`DifferentiableAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ContinuousAlternatingMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousAlternatingMap.instAddCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousAlternatingMap.instModule` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `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` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `Ring.toSemiring` `CommRing.toRing` `ContinuousAlternatingMap.instTopologicalSpace`	`DFunLike.coe` `ContinuousAlternatingMap.funLike` `extDeriv` `Finset.sum` `Finset.univ` `Fin.fintype` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `Monoid.toNatPow` `Int.instMonoid` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.funLike` `fderiv` `Fin.removeNth`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `smulCommClass_self` `extDerivWithin_apply` `DifferentiableAt.differentiableWithinAt` `PerfectSpace.not_isolated` `instPerfectSpace` `IsBoundedSMul.continuousSMul` `Finset.sum_congr` `fderivWithin_univ`
`extDeriv_constOfIsEmpty` 📖	mathematical	—	`extDeriv` `ContinuousAlternatingMap.constOfIsEmpty` `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` `Fin.isEmpty'` `DFunLike.coe` `Equiv` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `ContinuousAlternatingMap` `EquivLike.toFunLike` `Equiv.instEquivLike` `ContinuousAlternatingMap.ofSubsingleton` `fderiv` `SeminormedAddCommGroup.toAddCommGroup`	—	`Fin.isEmpty'` `extDerivWithin_constOfIsEmpty` `PerfectSpace.not_isolated` `instPerfectSpace` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `fderivWithin_univ`
`extDeriv_extDeriv` 📖	mathematical	`ContDiff` `ContinuousAlternatingMap` `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` `ContinuousAlternatingMap.instNormedAddCommGroup` `Fin.fintype` `ContinuousAlternatingMap.instNormedSpace` `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` `minSmoothness` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `WithTop.addMonoidWithOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `Nat.instAtLeastTwoHAddOfNat`	`extDeriv` `Pi.instZero` `ContinuousAlternatingMap.instZero`	—	`smulCommClass_self` `Nat.instAtLeastTwoHAddOfNat` `extDeriv_extDeriv_apply` `ContDiff.contDiffAt`
`extDeriv_extDeriv_apply` 📖	mathematical	`ContDiffAt` `ContinuousAlternatingMap` `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` `ContinuousAlternatingMap.instNormedAddCommGroup` `Fin.fintype` `ContinuousAlternatingMap.instNormedSpace` `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` `minSmoothness` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `WithTop.addMonoidWithOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `Nat.instAtLeastTwoHAddOfNat`	`extDeriv` `ContinuousAlternatingMap.instZero`	—	`smulCommClass_self` `Nat.instAtLeastTwoHAddOfNat` `extDerivWithin_extDerivWithin_apply` `ContDiffAt.contDiffWithinAt` `PerfectSpace.not_isolated` `instPerfectSpace` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `interior_univ` `IsClosed.closure_eq`
`extDeriv_fun_add` 📖	mathematical	`DifferentiableAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ContinuousAlternatingMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousAlternatingMap.instAddCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousAlternatingMap.instModule` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `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` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `Ring.toSemiring` `CommRing.toRing` `ContinuousAlternatingMap.instTopologicalSpace`	`extDeriv` `ContinuousAlternatingMap.instAdd` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `smulCommClass_self` `extDeriv_add`
`extDeriv_fun_smul` 📖	mathematical	—	`extDeriv` `Function.hasSMul` `ContinuousAlternatingMap` `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` `ContinuousAlternatingMap.instSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toIsBoundedSMul` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `Ring.toSemiring` `CommRing.toRing`	—	`extDeriv_smul`
`extDeriv_pullback` 📖	mathematical	`DifferentiableAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ContinuousAlternatingMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousAlternatingMap.instAddCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousAlternatingMap.instModule` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `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` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `Ring.toSemiring` `CommRing.toRing` `ContinuousAlternatingMap.instTopologicalSpace` `ContDiffAt` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `minSmoothness` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `WithTop.addMonoidWithOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `Nat.instAtLeastTwoHAddOfNat`	`extDeriv` `ContinuousAlternatingMap.compContinuousLinearMap` `fderiv` `AddCommGroup.toAddCommMonoid`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `smulCommClass_self` `Nat.instAtLeastTwoHAddOfNat` `extDerivWithin_pullback` `PerfectSpace.not_isolated` `instPerfectSpace` `IsBoundedSMul.continuousSMul` `interior_univ` `IsClosed.closure_eq`
`extDeriv_smul` 📖	mathematical	—	`extDeriv` `Function.hasSMul` `ContinuousAlternatingMap` `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` `ContinuousAlternatingMap.instSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toIsBoundedSMul` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `Ring.toSemiring` `CommRing.toRing`	—	`UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `smulCommClass_self` `extDerivWithin_smul` `PerfectSpace.not_isolated` `instPerfectSpace` `IsBoundedSMul.continuousSMul`

---

← Back to Index