RestrictScalars

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

Statistics

Metric	Count
Definitions	0
Theorems restrictScalars_iteratedFDeriv, restrictScalars_iteratedFDeriv_eventuallyEq, restrictScalars_iteratedFDerivWithin_eventuallyEq, fderivWithin_restrictScalars_comp	4
Total	4

ContDiffAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
restrictScalars_iteratedFDeriv 📖	mathematical	ContDiffAt WithTop ENat AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	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.restrictScalars Algebra.toSMul Semifield.toCommSemiring Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NormedAlgebra.toAlgebra iteratedFDeriv	—	Filter.EventuallyEq.eq_of_nhds restrictScalars_iteratedFDeriv_eventuallyEq
restrictScalars_iteratedFDeriv_eventuallyEq 📖	mathematical	ContDiffAt WithTop ENat AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	Filter.EventuallyEq 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 nhds ContinuousMultilinearMap.restrictScalars Algebra.toSMul Semifield.toCommSemiring Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NormedAlgebra.toAlgebra iteratedFDeriv	—	nhdsWithin_univ iteratedFDerivWithin_univ ContDiffWithinAt.restrictScalars_iteratedFDerivWithin_eventuallyEq NormedField.nhdsNE_neBot IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul

ContDiffWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
restrictScalars_iteratedFDerivWithin_eventuallyEq 📖	mathematical	ContDiffWithinAt WithTop ENat AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat UniqueDiffOn DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Set Set.instMembership	Filter.EventuallyEq ContinuousMultilinearMap ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid nhdsWithin ContinuousMultilinearMap.restrictScalars Algebra.toSMul Semifield.toCommSemiring Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NormedAlgebra.toAlgebra iteratedFDerivWithin	—	Filter.univ_mem' ContinuousMultilinearMap.ext of_le Nat.cast_le WithTop.addLeftMono IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid WithTop.zeroLEOneClass IsOrderedRing.toZeroLEOneClass WithTop.charZero Set.insert_eq_of_mem eventually Nat.cast_add Nat.cast_one Filter.mp_mem eventually_mem_nhdsWithin eventually_eventually_nhdsWithin SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self Filter.EventuallyEq.eq_of_nhdsWithin Filter.EventuallyEq.fderivWithin' Filter.EventuallyEq.eq_1 IsScalarTower.to_smulCommClass' LinearMap.IsScalarTower.compatibleSMul ContinuousMultilinearMap.instIsScalarTower fderivWithin_restrictScalars_comp differentiableWithinAt_iteratedFDerivWithin Nat.cast_lt IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd Nat.instIsOrderedAddMonoid contravariant_lt_of_covariant_le Nat.instZeroLEOneClass UniqueDiffOn.mono_field

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fderivWithin_restrictScalars_comp 📖	mathematical	DifferentiableWithinAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousMultilinearMap.instAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousMultilinearMap.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 ContinuousMultilinearMap.instTopologicalSpace UniqueDiffWithinAt	DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.funLike fderivWithin ContinuousMultilinearMap.restrictScalars Algebra.toSMul Semifield.toCommSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra IsScalarTower.to_smulCommClass' ContinuousLinearMap.restrictScalars LinearMap.IsScalarTower.compatibleSMul ContinuousMultilinearMap.instIsScalarTower	—	SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self IsScalarTower.to_smulCommClass' LinearMap.IsScalarTower.compatibleSMul ContinuousMultilinearMap.instIsScalarTower IsTopologicalAddGroup.toContinuousAdd IsBoundedSMul.continuousSMul RingHomCompTriple.ids fderiv_comp_fderivWithin ContinuousLinearMap.differentiableAt DifferentiableWithinAt.restrictScalars ContinuousLinearMap.fderiv ContinuousMultilinearMap.instIsTopologicalAddGroup SeminormedAddCommGroup.to_isUniformAddGroup ContinuousMultilinearMap.instIsBoundedSMul ContinuousMultilinearMap.instContinuousSMul ContinuousMultilinearMap.instT2Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace ContinuousMultilinearMap.ext DifferentiableWithinAt.restrictScalars_fderivWithin

---

← Back to Index