Poincare

📁 Source: Mathlib/MeasureTheory/Integral/CurveIntegral/Poincare.lean

Statistics

Metric	Count
Definitions	0
Theorems curveIntegral_add_curveIntegral_eq_of_diffContOnCl, curveIntegral_add_curveIntegral_eq_of_hasFDerivWithinAt, curveIntegral_add_curveIntegral_eq_of_hasFDerivWithinAt_off_countable, curveIntegral_segment_add_eq_of_hasFDerivWithinAt_symmetric, exists_forall_hasDerivWithinAt, exists_forall_hasFDerivAt_of_fderiv_symmetric, exists_forall_hasFDerivWithinAt_of_fderivWithin_symmetric, exists_forall_hasFDerivWithinAt_of_hasFDerivWithinAt_symmetric, hasFDerivWithinAt_curveIntegral_segment_of_hasFDerivWithinAt_symmetric	9
Total	9

ContinuousMap.Homotopy

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
curveIntegral_add_curveIntegral_eq_of_diffContOnCl 📖	mathematical	Set Set.instMembership DFunLike.coe ContinuousMap.Homotopy Set.Elem Real unitInterval instTopologicalSpaceSubtype UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup toContinuousMap Path Path.instFunLike Path.continuousMapClass instFunLike DiffContOnCl ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField ContinuousLinearMap.toNormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ContinuousLinearMap.toNormedSpace NontriviallyNormedField.toNormedField IsScalarTower.to_smulCommClass' Real.instCommSemiring NormedAlgebra.toAlgebra Real.normedField RCLike.toNormedAlgebra Real.isScalarTower NormedAddCommGroup.toAddCommGroup IsBoundedSMul.continuousSMul Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring AddCommGroup.toAddCommMonoid NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace SeminormedRing.toPseudoMetricSpace NormedRing.toRing NormedCommRing.toNormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Algebra.toSMul Ring.toSemiring NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal MonoidWithZero.toMonoid Semiring.toMonoidWithZero ContinuousLinearMap.funLike ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.addCommGroup ContinuousLinearMap.module UniformContinuousConstSMul.to_continuousConstSMul AddCommMonoid.toAddMonoid IsBoundedSMul.toUniformContinuousConstSMul fderivWithin ContDiffOn Prod.normedAddCommGroup Real.normedAddCommGroup Prod.normedSpace WithTop ENat instOfNatAtLeastTwo AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne CommSemiring.toSemiring instCommSemiringENat Nat.instAtLeastTwoHAddOfNat Set.IccExtend Real.linearOrder Real.instOne zero_le_one Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Real.instZeroLEOneClass ContinuousMap ContinuousMap.instFunLike ContinuousMap.compactOpen extend Set.Icc Prod.instPreorder Real.instPreorder Prod.instZero Prod.instOne	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup curveIntegral Set.Icc.instOne Real.partialOrder Real.instIsOrderedRing evalAt Set.Icc.instZero	—	Path.continuousMapClass Real.instIsOrderedRing RingHomIsometric.ids IsScalarTower.to_smulCommClass' Real.isScalarTower IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul Nat.instAtLeastTwoHAddOfNat zero_le_one Real.instZeroLEOneClass curveIntegral_add_curveIntegral_eq_of_hasFDerivWithinAt DifferentiableWithinAt.hasFDerivWithinAt DiffContOnCl.differentiableOn DiffContOnCl.continuousOn
curveIntegral_add_curveIntegral_eq_of_hasFDerivWithinAt 📖	mathematical	Set Set.instMembership DFunLike.coe ContinuousMap.Homotopy Set.Elem Real unitInterval instTopologicalSpaceSubtype UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup toContinuousMap Path Path.instFunLike Path.continuousMapClass instFunLike HasFDerivWithinAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousLinearMap.addCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.module Real.semiring IsScalarTower.to_smulCommClass' Real.instCommSemiring NormedAlgebra.toAlgebra SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing RCLike.toNormedAlgebra Real.isScalarTower NormedAddCommGroup.toAddCommGroup IsBoundedSMul.continuousSMul Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction AddCommGroup.toAddCommMonoid NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace SeminormedRing.toPseudoMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Algebra.toSMul Ring.toSemiring NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal MonoidWithZero.toMonoid Semiring.toMonoidWithZero UniformContinuousConstSMul.to_continuousConstSMul AddCommMonoid.toAddMonoid IsBoundedSMul.toUniformContinuousConstSMul IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup ContinuousLinearMap.topologicalSpace ContinuousOn closure ContinuousLinearMap.funLike ContinuousLinearMap.addCommMonoid ContDiffOn Prod.normedAddCommGroup Real.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField WithTop ENat instOfNatAtLeastTwo AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne CommSemiring.toSemiring instCommSemiringENat Nat.instAtLeastTwoHAddOfNat Set.IccExtend Real.linearOrder Real.instOne zero_le_one Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Real.instZeroLEOneClass ContinuousMap ContinuousMap.instFunLike ContinuousMap.compactOpen extend Set.Icc Prod.instPreorder Real.instPreorder Prod.instZero Prod.instOne	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup curveIntegral Set.Icc.instOne Real.partialOrder Real.instIsOrderedRing evalAt Set.Icc.instZero	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd IsScalarTower.to_smulCommClass' Real.isScalarTower IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul Path.continuousMapClass Real.instIsOrderedRing Nat.instAtLeastTwoHAddOfNat zero_le_one Real.instZeroLEOneClass curveIntegral_add_curveIntegral_eq_of_hasFDerivWithinAt_off_countable
curveIntegral_add_curveIntegral_eq_of_hasFDerivWithinAt_off_countable 📖	mathematical	Set Set.instMembership DFunLike.coe ContinuousMap.Homotopy Set.Elem Real unitInterval instTopologicalSpaceSubtype UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup toContinuousMap Path Path.instFunLike Path.continuousMapClass instFunLike HasFDerivWithinAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousLinearMap.addCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.module Real.semiring IsScalarTower.to_smulCommClass' Real.instCommSemiring NormedAlgebra.toAlgebra SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing RCLike.toNormedAlgebra Real.isScalarTower NormedAddCommGroup.toAddCommGroup IsBoundedSMul.continuousSMul Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction AddCommGroup.toAddCommMonoid NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace SeminormedRing.toPseudoMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Algebra.toSMul Ring.toSemiring NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal MonoidWithZero.toMonoid Semiring.toMonoidWithZero UniformContinuousConstSMul.to_continuousConstSMul AddCommMonoid.toAddMonoid IsBoundedSMul.toUniformContinuousConstSMul IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup ContinuousLinearMap.topologicalSpace ContinuousOn closure ContinuousLinearMap.funLike ContinuousLinearMap.addCommMonoid ContDiffOn Prod.normedAddCommGroup Real.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField WithTop ENat instOfNatAtLeastTwo AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne CommSemiring.toSemiring instCommSemiringENat Nat.instAtLeastTwoHAddOfNat Set.IccExtend Real.linearOrder Real.instOne zero_le_one Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Real.instZeroLEOneClass ContinuousMap ContinuousMap.instFunLike ContinuousMap.compactOpen extend Set.Icc Prod.instPreorder Real.instPreorder Prod.instZero Prod.instOne	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup curveIntegral Set.Icc.instOne Real.partialOrder Real.instIsOrderedRing evalAt Set.Icc.instZero	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd IsScalarTower.to_smulCommClass' Real.isScalarTower IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul Path.continuousMapClass Real.instIsOrderedRing Nat.instAtLeastTwoHAddOfNat zero_le_one Real.instZeroLEOneClass LinearMap.IsScalarTower.compatibleSMul curveIntegral_restrictScalars smulCommClass_self RingHomCompTriple.ids HasFDerivAt.comp_hasFDerivWithinAt RingHomIsometric.ids ContinuousLinearMap.hasFDerivAt Continuous.comp_continuousOn ContinuousLinearMap.continuous

Convex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
curveIntegral_segment_add_eq_of_hasFDerivWithinAt_symmetric 📖	mathematical	Convex Real Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction NormedSpace.toModule Real.normedField HasFDerivWithinAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField SeminormedAddCommGroup.toAddCommGroup ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.addCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.module IsScalarTower.to_smulCommClass' Real.instCommSemiring NormedAlgebra.toAlgebra SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing RCLike.toNormedAlgebra Real.isScalarTower NormedAddCommGroup.toAddCommGroup IsBoundedSMul.continuousSMul Real.pseudoMetricSpace Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGroup.toAddCommMonoid NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace SeminormedRing.toPseudoMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Algebra.toSMul Ring.toSemiring NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal MonoidWithZero.toMonoid Semiring.toMonoidWithZero UniformContinuousConstSMul.to_continuousConstSMul AddCommMonoid.toAddMonoid IsBoundedSMul.toUniformContinuousConstSMul IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup ContinuousLinearMap.topologicalSpace DFunLike.coe ContinuousLinearMap.funLike ContinuousLinearMap.addCommMonoid Set Set.instMembership	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup curveIntegral Path.segment	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd IsScalarTower.to_smulCommClass' Real.isScalarTower IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul Path.continuousMapClass Set.range_subset_iff lineMap_mem covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instIsOrderedRing ContinuousMap.Homotopy.curveIntegral_add_curveIntegral_eq_of_hasFDerivWithinAt Set.mem_range_self HasFDerivWithinAt.mono IsClosed.closure_eq IsCompact.isClosed isCompact_range instCompactSpaceProd compactSpace_Icc ConditionallyCompleteLinearOrder.toCompactIccSpace instOrderTopologyReal ContinuousMapClass.map_continuous ContinuousMap.HomotopyLike.toContinuousMapClass ContinuousMap.Homotopy.instHomotopyLike ContinuousWithinAt.mono HasFDerivWithinAt.continuousWithinAt RingHomIsometric.ids ContinuousLinearMap.topologicalAddGroup Set.mem_of_subset_of_mem tangentConeAt_mono zero_le_one Real.instZeroLEOneClass Set.Icc_prod_eq CanLift.prf Subtype.canLift Set.IccExtend.congr_simp ContinuousMap.Homotopy.extend_of_mem_I Subtype.coe_eta Set.IccExtend_val ContDiffOn.congr Nat.instAtLeastTwoHAddOfNat AffineMap.lineMap_apply_module ContDiffOn.add ContDiffOn.fun_smul IsScalarTower.left ContDiffOn.sub contDiffOn_const ContDiffOn.fst contDiffOn_fun_id ContDiffOn.smul_const ContDiffOn.snd AffineMap.lineMap_apply_one Path.cast_segment curveIntegral_cast AffineMap.lineMap_apply_zero Path.cast.congr_simp Path.segment_same curveIntegral_refl add_zero
exists_forall_hasDerivWithinAt 📖	mathematical	Convex Real Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing Algebra.toSMul Semifield.toCommSemiring Field.toSemifield NormedField.toField Real.normedField Ring.toSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra RCLike.toNormedAlgebra DifferentiableOn DenselyNormedField.toNontriviallyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing InnerProductSpace.toNormedSpace RCLike.innerProductSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace	HasDerivWithinAt IsBoundedSMul.continuousSMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring NontriviallyNormedField.toNormedField Module.toDistribMulAction AddCommGroup.toAddCommMonoid NormedSpace.toIsBoundedSMul	—	exists_forall_hasFDerivWithinAt_of_hasFDerivWithinAt_symmetric IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul RingHomIsometric.ids smulCommClass_self IsScalarTower.to_smulCommClass' Real.isScalarTower TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace LinearMap.IsScalarTower.compatibleSMul IsScalarTower.right ContinuousLinearMap.isScalarTower SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing IsTopologicalAddGroup.toContinuousAdd UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul ContinuousLinearMap.topologicalAddGroup Algebra.to_smulCommClass Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul ContinuousLinearMap.smulCommClass ContinuousLinearMap.continuousConstSMul HasFDerivAtFilter.restrictScalars HasFDerivAt.comp_hasDerivWithinAt ContinuousLinearMap.hasFDerivAt DifferentiableWithinAt.hasDerivWithinAt SMulCommClass.smul_comm
exists_forall_hasFDerivAt_of_fderiv_symmetric 📖	mathematical	Convex Real Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction NormedSpace.toModule Real.normedField IsOpen DifferentiableOn DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.addCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.module NontriviallyNormedField.toNormedField IsScalarTower.to_smulCommClass' Real.instCommSemiring NormedAlgebra.toAlgebra SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing RCLike.toNormedAlgebra Real.isScalarTower IsBoundedSMul.continuousSMul Real.pseudoMetricSpace Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGroup.toAddCommMonoid NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace SeminormedRing.toPseudoMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Algebra.toSMul Ring.toSemiring NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal MonoidWithZero.toMonoid Semiring.toMonoidWithZero UniformContinuousConstSMul.to_continuousConstSMul AddCommMonoid.toAddMonoid IsBoundedSMul.toUniformContinuousConstSMul ContinuousLinearMap.topologicalSpace DFunLike.coe ContinuousLinearMap.funLike fderiv	HasFDerivAt	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsScalarTower.to_smulCommClass' Real.isScalarTower IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul exists_forall_hasFDerivWithinAt_of_fderivWithin_symmetric fderivWithin_eq_fderiv IsTopologicalAddGroup.toContinuousAdd RingHomIsometric.ids ContinuousLinearMap.topologicalAddGroup ContinuousLinearMap.instT2Space IsOpen.uniqueDiffOn PerfectSpace.not_isolated instPerfectSpace DifferentiableOn.differentiableAt IsOpen.mem_nhds HasFDerivWithinAt.hasFDerivAt
exists_forall_hasFDerivWithinAt_of_fderivWithin_symmetric 📖	mathematical	Convex Real Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction NormedSpace.toModule Real.normedField DifferentiableOn DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.addCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.module NontriviallyNormedField.toNormedField IsScalarTower.to_smulCommClass' Real.instCommSemiring NormedAlgebra.toAlgebra SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing RCLike.toNormedAlgebra Real.isScalarTower IsBoundedSMul.continuousSMul Real.pseudoMetricSpace Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGroup.toAddCommMonoid NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace SeminormedRing.toPseudoMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Algebra.toSMul Ring.toSemiring NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal MonoidWithZero.toMonoid Semiring.toMonoidWithZero UniformContinuousConstSMul.to_continuousConstSMul AddCommMonoid.toAddMonoid IsBoundedSMul.toUniformContinuousConstSMul ContinuousLinearMap.topologicalSpace DFunLike.coe ContinuousLinearMap.funLike fderivWithin	HasFDerivWithinAt	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsScalarTower.to_smulCommClass' Real.isScalarTower IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul exists_forall_hasFDerivWithinAt_of_hasFDerivWithinAt_symmetric DifferentiableWithinAt.hasFDerivWithinAt
exists_forall_hasFDerivWithinAt_of_hasFDerivWithinAt_symmetric 📖	—	Convex Real Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction NormedSpace.toModule Real.normedField HasFDerivWithinAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField SeminormedAddCommGroup.toAddCommGroup ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.addCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.module IsScalarTower.to_smulCommClass' Real.instCommSemiring NormedAlgebra.toAlgebra SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing RCLike.toNormedAlgebra Real.isScalarTower NormedAddCommGroup.toAddCommGroup IsBoundedSMul.continuousSMul Real.pseudoMetricSpace Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGroup.toAddCommMonoid NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace SeminormedRing.toPseudoMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Algebra.toSMul Ring.toSemiring NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal MonoidWithZero.toMonoid Semiring.toMonoidWithZero UniformContinuousConstSMul.to_continuousConstSMul AddCommMonoid.toAddMonoid IsBoundedSMul.toUniformContinuousConstSMul IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup ContinuousLinearMap.topologicalSpace DFunLike.coe ContinuousLinearMap.funLike ContinuousLinearMap.addCommMonoid	—	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd IsScalarTower.to_smulCommClass' Real.isScalarTower IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul Set.eq_empty_or_nonempty AddTorsor.nonempty hasFDerivWithinAt_curveIntegral_segment_of_hasFDerivWithinAt_symmetric
hasFDerivWithinAt_curveIntegral_segment_of_hasFDerivWithinAt_symmetric 📖	mathematical	Convex Real Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction NormedSpace.toModule Real.normedField HasFDerivWithinAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField SeminormedAddCommGroup.toAddCommGroup ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.addCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.module IsScalarTower.to_smulCommClass' Real.instCommSemiring NormedAlgebra.toAlgebra SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing RCLike.toNormedAlgebra Real.isScalarTower NormedAddCommGroup.toAddCommGroup IsBoundedSMul.continuousSMul Real.pseudoMetricSpace Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGroup.toAddCommMonoid NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace SeminormedRing.toPseudoMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Algebra.toSMul Ring.toSemiring NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal MonoidWithZero.toMonoid Semiring.toMonoidWithZero UniformContinuousConstSMul.to_continuousConstSMul AddCommMonoid.toAddMonoid IsBoundedSMul.toUniformContinuousConstSMul IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup ContinuousLinearMap.topologicalSpace DFunLike.coe ContinuousLinearMap.funLike ContinuousLinearMap.addCommMonoid Set Set.instMembership	curveIntegral Path.segment	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd IsScalarTower.to_smulCommClass' Real.isScalarTower IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul HasFDerivWithinAt.const_add HasFDerivWithinAt.curveIntegral_segment_source HasFDerivWithinAt.continuousWithinAt RingHomIsometric.ids ContinuousLinearMap.topologicalAddGroup HasFDerivWithinAt.congr' curveIntegral_segment_add_eq_of_hasFDerivWithinAt_symmetric

---

← Back to Index