Star

📁 Source: Mathlib/Analysis/Calculus/FDeriv/Star.lean

Statistics

Metric	Count
Definitions	0
Theorems star_star, star_star, differentiableAt_star_iff, differentiableOn_star_iff, differentiableWithinAt_star_iff, differentiable_star_iff, fderivWithin_star, fderiv_star	8
Total	8

DifferentiableAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
star_star 📖	mathematical	DifferentiableAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	HasFDerivAt.differentiableAt RingHomInvPair.triples₂ RingHomInvPair.instStarRingEnd RingHomCompTriple.right_ids HasFDerivAt.star_star hasFDerivAt

HasFDerivAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
star_star 📖	mathematical	HasFDerivAt SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousLinearMap.comp DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField CommSemiring.toSemiring Semifield.toCommSemiring starRingEnd RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid RingHomInvPair.triples₂ RingHomInvPair.instStarRingEnd ContinuousLinearEquiv.toContinuousLinearMap starL ESeminormedAddCommMonoid.toAddCommMonoid RingHomCompTriple.right_ids	—	comp_semilinear RingHomIsometric.starRingEnd RingHomInvPair.instStarRingEnd star_star

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
differentiableAt_star_iff 📖	mathematical	—	DifferentiableAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	ContinuousLinearEquiv.comp_differentiableAt_iff
differentiableOn_star_iff 📖	mathematical	—	DifferentiableOn NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	ContinuousLinearEquiv.comp_differentiableOn_iff
differentiableWithinAt_star_iff 📖	mathematical	—	DifferentiableWithinAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	ContinuousLinearEquiv.comp_differentiableWithinAt_iff
differentiable_star_iff 📖	mathematical	—	Differentiable NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	ContinuousLinearEquiv.comp_differentiable_iff
fderivWithin_star 📖	mathematical	UniqueDiffWithinAt DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	fderivWithin Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousLinearMap.comp CommSemiring.toSemiring Semifield.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid RingHomCompTriple.ids ContinuousLinearEquiv.toContinuousLinearMap RingHomInvPair.ids starL' SeminormedAddCommGroup.toAddCommGroup	—	ContinuousLinearEquiv.comp_fderivWithin
fderiv_star 📖	mathematical	—	fderiv NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousLinearMap.comp CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid RingHomCompTriple.ids ContinuousLinearEquiv.toContinuousLinearMap RingHomInvPair.ids starL' SeminormedAddCommGroup.toAddCommGroup	—	ContinuousLinearEquiv.comp_fderiv

---

← Back to Index