Documentation Verification Report

Transform

📁 Source: Mathlib/Geometry/Manifold/IntegralCurve/Transform.lean

Statistics

Metric	Count
Definitions	0
Theorems `comp_add`, `comp_mul`, `comp_add`, `comp_mul_ne_zero`, `comp_add`, `comp_mul`, `isMIntegralCurveAt_comp_add`, `isMIntegralCurveAt_comp_mul_ne_zero`, `isMIntegralCurveAt_comp_sub`, `isMIntegralCurveOn_comp_add`, `isMIntegralCurveOn_comp_mul_ne_zero`, `isMIntegralCurveOn_comp_sub`, `isMIntegralCurve_comp_add`, `isMIntegralCurve_comp_mul_ne_zero`, `isMIntegralCurve_comp_sub`, `isMIntegralCurve_const`	16
Total	16

IsMIntegralCurve

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_add` 📖	mathematical	`IsMIntegralCurve`	`Real` `Real.instAdd`	—	`isMIntegralCurve_iff_isMIntegralCurveOn` `IsMIntegralCurveOn.comp_add`
`comp_mul` 📖	mathematical	`IsMIntegralCurve`	`Real` `Real.instMul` `Pi.instSMul` `TangentSpace` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `SMulZeroClass.toSMul` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroupTangentSpace` `DistribSMul.toSMulZeroClass` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `instModuleTangentSpace`	—	`isMIntegralCurve_iff_isMIntegralCurveOn` `IsMIntegralCurveOn.comp_mul`

IsMIntegralCurveAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_add` 📖	mathematical	`IsMIntegralCurveAt`	`Real` `Real.instAdd` `Real.instSub`	—	`isMIntegralCurveAt_iff'` `Metric.ball.eq_1` `add_sub_right_comm` `IsMIntegralCurveOn.comp_add`
`comp_mul_ne_zero` 📖	mathematical	`IsMIntegralCurveAt`	`Real` `Real.instMul` `Pi.instSMul` `TangentSpace` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `SMulZeroClass.toSMul` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroupTangentSpace` `DistribSMul.toSMulZeroClass` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `instModuleTangentSpace` `DivInvMonoid.toDiv` `Real.instDivInvMonoid`	—	`isMIntegralCurveAt_iff'` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Mathlib.Meta.Positivity.abs_pos_of_ne_zero` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Set.ext` `Set.mem_setOf_eq` `Metric.mem_ball` `Real.dist_eq` `lt_div_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `abs_pos` `abs_mul` `Real.instIsOrderedRing` `sub_mul` `div_mul_cancel₀` `IsMIntegralCurveOn.comp_mul`

IsMIntegralCurveOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_add` 📖	mathematical	`IsMIntegralCurveOn`	`Real` `Real.instAdd` `setOf` `Set` `Set.instMembership`	—	`RingHomCompTriple.ids` `ContinuousLinearMap.comp_id` `HasMFDerivWithinAt.comp` `Continuous.continuousWithinAt` `continuous_add_right` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `PartialEquiv.trans_refl` `Set.range_id` `Set.inter_univ` `HasFDerivWithinAt.add_const` `hasFDerivWithinAt_id` `subset_rfl` `Set.instReflSubset`
`comp_mul` 📖	mathematical	`IsMIntegralCurveOn`	`Real` `Real.instMul` `Pi.instSMul` `TangentSpace` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `SMulZeroClass.toSMul` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroupTangentSpace` `DistribSMul.toSMulZeroClass` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `instModuleTangentSpace` `setOf` `Set` `Set.instMembership`	—	`Pi.smul_apply` `ContinuousLinearMap.one_apply` `RingHomCompTriple.ids` `IsScalarTower.left` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `ContinuousLinearMap.smulRight_comp_smulRight` `HasMFDerivWithinAt.comp` `Continuous.continuousWithinAt` `continuous_mul_right` `IsTopologicalSemiring.toContinuousMul` `PartialEquiv.trans_refl` `Set.range_id` `Set.inter_univ` `HasFDerivWithinAt.mul_const'` `hasFDerivWithinAt_id` `subset_rfl` `Set.instReflSubset`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isMIntegralCurveAt_comp_add` 📖	mathematical	—	`IsMIntegralCurveAt` `Real` `Real.instAdd` `Real.instSub`	—	`IsMIntegralCurveAt.comp_add` `neg_add_cancel_right` `sub_neg_eq_add` `sub_add_cancel`
`isMIntegralCurveAt_comp_mul_ne_zero` 📖	mathematical	—	`IsMIntegralCurveAt` `Real` `Real.instMul` `Pi.instSMul` `TangentSpace` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `SMulZeroClass.toSMul` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroupTangentSpace` `DistribSMul.toSMulZeroClass` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `instModuleTangentSpace` `DivInvMonoid.toDiv` `Real.instDivInvMonoid`	—	`IsMIntegralCurveAt.comp_mul_ne_zero` `mul_assoc` `inv_mul_eq_div` `div_self` `mul_one` `smul_smul` `one_smul` `div_inv_eq_mul` `div_mul_cancel₀` `inv_ne_zero`
`isMIntegralCurveAt_comp_sub` 📖	mathematical	—	`IsMIntegralCurveAt` `Real` `Real.instSub` `Real.instAdd`	—	`sub_neg_eq_add` `isMIntegralCurveAt_comp_add`
`isMIntegralCurveOn_comp_add` 📖	mathematical	—	`IsMIntegralCurveOn` `Real` `Real.instAdd` `setOf` `Set` `Set.instMembership`	—	`IsMIntegralCurveOn.comp_add` `neg_add_cancel_right`
`isMIntegralCurveOn_comp_mul_ne_zero` 📖	mathematical	—	`IsMIntegralCurveOn` `Real` `Real.instMul` `Pi.instSMul` `TangentSpace` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `SMulZeroClass.toSMul` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroupTangentSpace` `DistribSMul.toSMulZeroClass` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `instModuleTangentSpace` `setOf` `Set` `Set.instMembership`	—	`IsMIntegralCurveOn.comp_mul` `mul_assoc` `inv_mul_eq_div` `div_self` `mul_one` `smul_smul` `one_smul`
`isMIntegralCurveOn_comp_sub` 📖	mathematical	—	`IsMIntegralCurveOn` `Real` `Real.instSub` `setOf` `Set` `Set.instMembership`	—	`isMIntegralCurveOn_comp_add`
`isMIntegralCurve_comp_add` 📖	mathematical	—	`IsMIntegralCurve` `Real` `Real.instAdd`	—	`IsMIntegralCurve.comp_add` `neg_add_cancel_right`
`isMIntegralCurve_comp_mul_ne_zero` 📖	mathematical	—	`IsMIntegralCurve` `Real` `Real.instMul` `Pi.instSMul` `TangentSpace` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `SMulZeroClass.toSMul` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroupTangentSpace` `DistribSMul.toSMulZeroClass` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `instModuleTangentSpace`	—	`IsMIntegralCurve.comp_mul` `mul_assoc` `inv_mul_eq_div` `div_self` `mul_one` `smul_smul` `one_smul`
`isMIntegralCurve_comp_sub` 📖	mathematical	—	`IsMIntegralCurve` `Real` `Real.instSub`	—	`isMIntegralCurve_comp_add`
`isMIntegralCurve_const` 📖	mathematical	`TangentSpace` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroupTangentSpace`	`IsMIntegralCurve`	—	`IsScalarTower.left` `ContinuousLinearMap.smulRight_one_eq_toSpanSingleton` `ContinuousLinearMap.toSpanSingleton_zero` `hasMFDerivAt_const`

---

← Back to Index