Const

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

Statistics

Metric	Count
Definitions	0
Theorems fderiv, fderiv_apply, of_notMem_tsupport, of_notMem_tsupport, of_notMem_tsupport, differentiableOn, differentiableAt_const, differentiableAt_intCast, differentiableAt_natCast, differentiableAt_ofNat, differentiableAt_of_isInvertible_fderiv, differentiableAt_one, differentiableAt_zero, differentiableOn_const, differentiableOn_intCast, differentiableOn_natCast, differentiableOn_ofNat, differentiableOn_one, differentiableOn_singleton, differentiableOn_zero, differentiableWithinAt_const, differentiableWithinAt_intCast, differentiableWithinAt_natCast, differentiableWithinAt_ofNat, differentiableWithinAt_of_isInvertible_fderivWithin, differentiableWithinAt_one, differentiableWithinAt_zero, differentiable_const, differentiable_intCast, differentiable_natCast, differentiable_ofNat, differentiable_of_subsingleton, differentiable_one, differentiable_zero, fderivWithin_const, fderivWithin_const_apply, fderivWithin_fun_const, fderivWithin_intCast, fderivWithin_natCast, fderivWithin_ofNat, fderivWithin_one, fderivWithin_zero, fderiv_const, fderiv_const_apply, fderiv_fun_const, fderiv_intCast, fderiv_natCast, fderiv_ofNat, fderiv_of_notMem_tsupport, fderiv_one, fderiv_zero, hasFDerivAtFilter_const, hasFDerivAtFilter_intCast, hasFDerivAtFilter_natCast, hasFDerivAtFilter_ofNat, hasFDerivAtFilter_one, hasFDerivAtFilter_zero, hasFDerivAt_const, hasFDerivAt_intCast, hasFDerivAt_natCast, hasFDerivAt_ofNat, hasFDerivAt_of_subsingleton, hasFDerivAt_one, hasFDerivAt_zero, hasFDerivAt_zero_of_eventually_const, hasFDerivWithinAt_const, hasFDerivWithinAt_intCast, hasFDerivWithinAt_natCast, hasFDerivWithinAt_ofNat, hasFDerivWithinAt_of_subsingleton, hasFDerivWithinAt_one, hasFDerivWithinAt_singleton, hasFDerivWithinAt_zero, hasStrictFDerivAt_const, hasStrictFDerivAt_intCast, hasStrictFDerivAt_natCast, hasStrictFDerivAt_ofNat, hasStrictFDerivAt_one, hasStrictFDerivAt_zero, support_fderiv_subset, tsupport_fderiv_apply_subset, tsupport_fderiv_subset	82
Total	82

HasCompactSupport

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fderiv 📖	mathematical	HasCompactSupport NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.zero fderiv	—	mono' support_fderiv_subset
fderiv_apply 📖	mathematical	HasCompactSupport NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.funLike fderiv	—	IsCompact.of_isClosed_subset isClosed_tsupport tsupport_fderiv_apply_subset

HasFDerivAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_notMem_tsupport 📖	mathematical	Set Set.instMembership tsupport NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	HasFDerivAt ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.zero	—	HasStrictFDerivAt.hasFDerivAt HasStrictFDerivAt.of_notMem_tsupport

HasFDerivWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_notMem_tsupport 📖	mathematical	Set Set.instMembership tsupport NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	HasFDerivWithinAt ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.zero	—	HasFDerivAt.hasFDerivWithinAt HasFDerivAt.of_notMem_tsupport

HasStrictFDerivAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_notMem_tsupport 📖	mathematical	Set Set.instMembership tsupport NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	HasStrictFDerivAt ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.zero	—	congr_of_eventuallyEq hasStrictFDerivAt_const Filter.EventuallyEq.symm notMem_tsupport_iff_eventuallyEq

Set.Subsingleton

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
differentiableOn 📖	mathematical	Set.Subsingleton	DifferentiableOn	—	induction_on differentiableOn_empty differentiableOn_singleton

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
differentiableAt_const 📖	mathematical	—	DifferentiableAt	—	hasFDerivAt_const
differentiableAt_intCast 📖	mathematical	—	DifferentiableAt Pi.instIntCast	—	differentiableAt_const
differentiableAt_natCast 📖	mathematical	—	DifferentiableAt Pi.instNatCast	—	differentiableAt_const
differentiableAt_ofNat 📖	mathematical	—	DifferentiableAt	—	differentiableAt_const
differentiableAt_of_isInvertible_fderiv 📖	mathematical	ContinuousLinearMap.IsInvertible DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid fderiv	DifferentiableAt	—	differentiableWithinAt_of_isInvertible_fderivWithin
differentiableAt_one 📖	mathematical	—	DifferentiableAt Pi.instOne	—	differentiableAt_const
differentiableAt_zero 📖	mathematical	—	DifferentiableAt Pi.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	differentiableAt_const
differentiableOn_const 📖	mathematical	—	DifferentiableOn	—	Differentiable.differentiableOn differentiable_const
differentiableOn_intCast 📖	mathematical	—	DifferentiableOn Pi.instIntCast	—	differentiableOn_const
differentiableOn_natCast 📖	mathematical	—	DifferentiableOn Pi.instNatCast	—	differentiableOn_const
differentiableOn_ofNat 📖	mathematical	—	DifferentiableOn	—	differentiableOn_const
differentiableOn_one 📖	mathematical	—	DifferentiableOn Pi.instOne	—	differentiableOn_const
differentiableOn_singleton 📖	mathematical	—	DifferentiableOn Set Set.instSingletonSet	—	HasFDerivWithinAt.differentiableWithinAt hasFDerivWithinAt_singleton
differentiableOn_zero 📖	mathematical	—	DifferentiableOn Pi.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	differentiableOn_const
differentiableWithinAt_const 📖	mathematical	—	DifferentiableWithinAt	—	DifferentiableAt.differentiableWithinAt differentiableAt_const
differentiableWithinAt_intCast 📖	mathematical	—	DifferentiableWithinAt Pi.instIntCast	—	differentiableWithinAt_const
differentiableWithinAt_natCast 📖	mathematical	—	DifferentiableWithinAt Pi.instNatCast	—	differentiableWithinAt_const
differentiableWithinAt_ofNat 📖	mathematical	—	DifferentiableWithinAt	—	differentiableWithinAt_const
differentiableWithinAt_of_isInvertible_fderivWithin 📖	mathematical	ContinuousLinearMap.IsInvertible DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid fderivWithin	DifferentiableWithinAt	—	Mathlib.Tactic.Contrapose.contrapose₁ fderivWithin_zero_of_not_differentiableWithinAt Mathlib.Tactic.Contrapose.contrapose₄ ContinuousLinearMap.isInvertible_zero_iff DifferentiableAt.differentiableWithinAt HasFDerivAt.differentiableAt hasFDerivAt_of_subsingleton
differentiableWithinAt_one 📖	mathematical	—	DifferentiableWithinAt Pi.instOne	—	differentiableWithinAt_const
differentiableWithinAt_zero 📖	mathematical	—	DifferentiableWithinAt Pi.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	differentiableWithinAt_const
differentiable_const 📖	mathematical	—	Differentiable	—	differentiableAt_const
differentiable_intCast 📖	mathematical	—	Differentiable Pi.instIntCast	—	differentiable_const
differentiable_natCast 📖	mathematical	—	Differentiable Pi.instNatCast	—	differentiable_const
differentiable_ofNat 📖	mathematical	—	Differentiable	—	differentiable_const
differentiable_of_subsingleton 📖	mathematical	—	Differentiable	—	HasFDerivAt.differentiableAt hasFDerivAt_of_subsingleton
differentiable_one 📖	mathematical	—	Differentiable Pi.instOne	—	differentiable_const
differentiable_zero 📖	mathematical	—	Differentiable Pi.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	differentiable_const
fderivWithin_const 📖	mathematical	—	fderivWithin Pi.instZero ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.zero	—	fderivWithin_fun_const
fderivWithin_const_apply 📖	mathematical	—	fderivWithin ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.zero	—	fderivWithin_def hasFDerivWithinAt_const
fderivWithin_fun_const 📖	mathematical	—	fderivWithin Pi.instZero ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.zero	—	ContinuousLinearMap.ext fderivWithin_const_apply Pi.zero_apply
fderivWithin_intCast 📖	mathematical	—	fderivWithin Pi.instIntCast Pi.instZero ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.zero	—	fderivWithin_const
fderivWithin_natCast 📖	mathematical	—	fderivWithin Pi.instNatCast Pi.instZero ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.zero	—	fderivWithin_const
fderivWithin_ofNat 📖	mathematical	—	fderivWithin Pi.instZero ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.zero	—	fderivWithin_const
fderivWithin_one 📖	mathematical	—	fderivWithin Pi.instOne Pi.instZero ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.zero	—	fderivWithin_const
fderivWithin_zero 📖	mathematical	—	fderivWithin Pi.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.zero	—	fderivWithin_const
fderiv_const 📖	mathematical	—	fderiv Pi.instZero ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.zero	—	fderiv_fun_const
fderiv_const_apply 📖	mathematical	—	fderiv ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.zero	—	fderiv_def fderivWithin_const_apply
fderiv_fun_const 📖	mathematical	—	fderiv Pi.instZero ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.zero	—	fderivWithin_univ fderivWithin_fun_const
fderiv_intCast 📖	mathematical	—	fderiv Pi.instIntCast Pi.instZero ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.zero	—	fderiv_const
fderiv_natCast 📖	mathematical	—	fderiv Pi.instNatCast Pi.instZero ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.zero	—	fderiv_const
fderiv_ofNat 📖	mathematical	—	fderiv Pi.instZero ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.zero	—	fderiv_const
fderiv_of_notMem_tsupport 📖	mathematical	Set Set.instMembership tsupport NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	fderiv ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.zero	—	Filter.EventuallyEq.fderiv_eq notMem_tsupport_iff_eventuallyEq fderiv_zero
fderiv_one 📖	mathematical	—	fderiv Pi.instOne Pi.instZero ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.zero	—	fderiv_const
fderiv_zero 📖	mathematical	—	fderiv Pi.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.zero	—	fderiv_const
hasFDerivAtFilter_const 📖	mathematical	—	HasFDerivAtFilter ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.zero	—	Asymptotics.IsLittleOTVS.congr_left Asymptotics.IsLittleOTVS.zero sub_self
hasFDerivAtFilter_intCast 📖	mathematical	—	HasFDerivAtFilter Pi.instIntCast ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.zero	—	hasFDerivAtFilter_const
hasFDerivAtFilter_natCast 📖	mathematical	—	HasFDerivAtFilter Pi.instNatCast ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.zero	—	hasFDerivAtFilter_const
hasFDerivAtFilter_ofNat 📖	mathematical	—	HasFDerivAtFilter ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.zero	—	hasFDerivAtFilter_const
hasFDerivAtFilter_one 📖	mathematical	—	HasFDerivAtFilter Pi.instOne ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.zero	—	hasFDerivAtFilter_const
hasFDerivAtFilter_zero 📖	mathematical	—	HasFDerivAtFilter Pi.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.zero	—	hasFDerivAtFilter_const
hasFDerivAt_const 📖	mathematical	—	HasFDerivAt ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.zero	—	hasFDerivAtFilter_const
hasFDerivAt_intCast 📖	mathematical	—	HasFDerivAt Pi.instIntCast ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.zero	—	hasFDerivAt_const
hasFDerivAt_natCast 📖	mathematical	—	HasFDerivAt Pi.instNatCast ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.zero	—	hasFDerivAt_const
hasFDerivAt_ofNat 📖	mathematical	—	HasFDerivAt ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.zero	—	hasFDerivAt_const
hasFDerivAt_of_subsingleton 📖	mathematical	—	HasFDerivAt ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.zero	—	hasFDerivWithinAt_univ Set.Subsingleton.eq_singleton_of_mem Set.subsingleton_univ Set.mem_univ hasFDerivWithinAt_singleton
hasFDerivAt_one 📖	mathematical	—	HasFDerivAt Pi.instOne ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.zero	—	hasFDerivAt_const
hasFDerivAt_zero 📖	mathematical	—	HasFDerivAt Pi.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.zero	—	hasFDerivAt_const
hasFDerivAt_zero_of_eventually_const 📖	mathematical	Filter.EventuallyEq nhds	HasFDerivAt ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.zero	—	HasFDerivAt.congr_of_eventuallyEq hasFDerivAt_const
hasFDerivWithinAt_const 📖	mathematical	—	HasFDerivWithinAt ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.zero	—	hasFDerivAtFilter_const
hasFDerivWithinAt_intCast 📖	mathematical	—	HasFDerivWithinAt Pi.instIntCast ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.zero	—	hasFDerivWithinAt_const
hasFDerivWithinAt_natCast 📖	mathematical	—	HasFDerivWithinAt Pi.instNatCast ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.zero	—	hasFDerivWithinAt_const
hasFDerivWithinAt_ofNat 📖	mathematical	—	HasFDerivWithinAt ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.zero	—	hasFDerivWithinAt_const
hasFDerivWithinAt_of_subsingleton 📖	mathematical	—	HasFDerivWithinAt ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.zero	—	Set.eq_empty_or_singleton_of_subsingleton HasFDerivWithinAt.singleton T2Space.t1Space TopologicalSpace.t2Space_of_metrizableSpace TopologicalSpace.DiscreteTopology.metrizableSpace Subsingleton.discreteTopology
hasFDerivWithinAt_one 📖	mathematical	—	HasFDerivWithinAt Pi.instOne ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.zero	—	hasFDerivWithinAt_const
hasFDerivWithinAt_singleton 📖	mathematical	—	HasFDerivWithinAt ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.zero Set Set.instSingletonSet	—	HasFDerivWithinAt.of_not_accPt accPt_iff_clusterPt Filter.inf_principal Set.inter_singleton_of_notMem Filter.principal_empty inf_of_le_right
hasFDerivWithinAt_zero 📖	mathematical	—	HasFDerivWithinAt Pi.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.zero	—	hasFDerivWithinAt_const
hasStrictFDerivAt_const 📖	mathematical	—	HasStrictFDerivAt ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.zero	—	Asymptotics.IsLittleOTVS.congr_left Asymptotics.IsLittleOTVS.zero sub_self
hasStrictFDerivAt_intCast 📖	mathematical	—	HasStrictFDerivAt Pi.instIntCast ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.zero	—	hasStrictFDerivAt_const
hasStrictFDerivAt_natCast 📖	mathematical	—	HasStrictFDerivAt Pi.instNatCast ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.zero	—	hasStrictFDerivAt_const
hasStrictFDerivAt_ofNat 📖	mathematical	—	HasStrictFDerivAt ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.zero	—	hasStrictFDerivAt_const
hasStrictFDerivAt_one 📖	mathematical	—	HasStrictFDerivAt Pi.instOne ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.zero	—	hasStrictFDerivAt_const
hasStrictFDerivAt_zero 📖	mathematical	—	HasStrictFDerivAt Pi.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.zero	—	hasStrictFDerivAt_const
support_fderiv_subset 📖	mathematical	—	Set Set.instHasSubset Function.support ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.zero fderiv tsupport NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	not_imp_not Function.notMem_support fderiv_of_notMem_tsupport
tsupport_fderiv_apply_subset 📖	mathematical	—	Set Set.instHasSubset tsupport NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.funLike fderiv	—	HasSubset.Subset.trans Set.instIsTransSubset tsupport_comp_subset tsupport_fderiv_subset
tsupport_fderiv_subset 📖	mathematical	—	Set Set.instHasSubset tsupport ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.zero fderiv NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	closure_minimal support_fderiv_subset isClosed_closure

---

← Back to Index