Transform

📁 Source: Mathlib/Analysis/ODE/Transform.lean

Statistics

Metric	Count
Definitions	0
Theorems comp_add, comp_mul, comp_sub, comp_add, comp_mul_ne_zero, comp_sub, comp_add, comp_mul, comp_sub, isIntegralCurveAt_comp_add, isIntegralCurveAt_comp_mul_ne_zero, isIntegralCurveAt_comp_sub, isIntegralCurveOn_comp_add, isIntegralCurveOn_comp_mul_ne_zero, isIntegralCurveOn_comp_sub, isIntegralCurve_comp_add, isIntegralCurve_comp_mul_ne_zero, isIntegralCurve_comp_sub, isIntegralCurve_const	19
Total	19

IsIntegralCurve

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_add 📖	mathematical	IsIntegralCurve	IsIntegralCurve Real Real.instAdd	—	isIntegralCurveOn_univ Set.vadd_set_univ IsIntegralCurveOn.comp_add
comp_mul 📖	mathematical	IsIntegralCurve	IsIntegralCurve Real Real.instMul Function.hasSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField	—	isIntegralCurveOn_univ IsIntegralCurveOn.comp_mul
comp_sub 📖	mathematical	IsIntegralCurve	IsIntegralCurve Real Real.instSub	—	isIntegralCurve_comp_sub

IsIntegralCurveAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_add 📖	mathematical	IsIntegralCurveAt	IsIntegralCurveAt Real Real.instAdd Real.instSub	—	isIntegralCurveAt_comp_add
comp_mul_ne_zero 📖	mathematical	IsIntegralCurveAt	IsIntegralCurveAt Real Real.instMul Function.hasSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField DivInvMonoid.toDiv Real.instDivInvMonoid	—	isIntegralCurveAt_iff_exists_pos 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₀ IsIntegralCurveOn.comp_mul
comp_sub 📖	mathematical	IsIntegralCurveAt	IsIntegralCurveAt Real Real.instSub Real.instAdd	—	isIntegralCurveAt_comp_sub

IsIntegralCurveOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_add 📖	mathematical	IsIntegralCurveOn	IsIntegralCurveOn Real Real.instAdd HVAdd.hVAdd Set instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup Real.instAddMonoid AddAction.toAddSemigroupAction AddTorsor.toAddAction Real.instAddGroup addGroupIsAddTorsor Real.instNeg	—	hasDerivWithinAt_iff_hasFDerivWithinAt hasFDerivWithinAt_comp_add_right vadd_neg_vadd add_comm vadd_eq_add neg_neg Set.mem_vadd_set_iff_neg_vadd_mem
comp_mul 📖	mathematical	IsIntegralCurveOn	IsIntegralCurveOn Real Real.instMul Function.hasSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField setOf Set Set.instMembership	—	HasDerivWithinAt.scomp IsScalarTower.left HasDerivAt.hasDerivWithinAt hasDerivAt_mul_const
comp_sub 📖	mathematical	IsIntegralCurveOn	IsIntegralCurveOn Real Real.instSub HVAdd.hVAdd Set instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup Real.instAddMonoid AddAction.toAddSemigroupAction AddTorsor.toAddAction Real.instAddGroup addGroupIsAddTorsor	—	isIntegralCurveOn_comp_sub

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isIntegralCurveAt_comp_add 📖	mathematical	—	IsIntegralCurveAt Real Real.instAdd Real.instSub	—	Metric.vadd_ball NormedAddGroup.to_isIsometricVAdd neg_add_eq_sub isIntegralCurveOn_comp_add
isIntegralCurveAt_comp_mul_ne_zero 📖	mathematical	—	IsIntegralCurveAt Real Real.instMul Function.hasSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField DivInvMonoid.toDiv Real.instDivInvMonoid	—	mul_assoc inv_mul_eq_div div_self mul_one smul_smul one_smul div_inv_eq_mul div_mul_cancel₀ IsIntegralCurveAt.comp_mul_ne_zero inv_ne_zero
isIntegralCurveAt_comp_sub 📖	mathematical	—	IsIntegralCurveAt Real Real.instSub Real.instAdd	—	sub_neg_eq_add isIntegralCurveAt_comp_add
isIntegralCurveOn_comp_add 📖	mathematical	—	IsIntegralCurveOn Real Real.instAdd HVAdd.hVAdd Set instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup Real.instAddMonoid AddAction.toAddSemigroupAction AddTorsor.toAddAction Real.instAddGroup addGroupIsAddTorsor Real.instNeg	—	neg_add_cancel_right neg_neg vadd_neg_vadd IsIntegralCurveOn.comp_add
isIntegralCurveOn_comp_mul_ne_zero 📖	mathematical	—	IsIntegralCurveOn Real Real.instMul Function.hasSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField Set Set.smulSet Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Real.instInv	—	Set.ext Set.mem_inv_smul_set_iff₀ smul_eq_mul mul_comm mul_assoc inv_mul_eq_div div_self mul_one smul_smul one_smul smul_inv_smul₀ IsIntegralCurveOn.comp_mul
isIntegralCurveOn_comp_sub 📖	mathematical	—	IsIntegralCurveOn Real Real.instSub HVAdd.hVAdd Set instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup Real.instAddMonoid AddAction.toAddSemigroupAction AddTorsor.toAddAction Real.instAddGroup addGroupIsAddTorsor	—	neg_neg isIntegralCurveOn_comp_add
isIntegralCurve_comp_add 📖	mathematical	—	IsIntegralCurve Real Real.instAdd	—	Set.vadd_set_univ isIntegralCurveOn_comp_add
isIntegralCurve_comp_mul_ne_zero 📖	mathematical	—	IsIntegralCurve Real Real.instMul Function.hasSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField	—	mul_assoc inv_mul_eq_div div_self mul_one smul_smul one_smul IsIntegralCurve.comp_mul
isIntegralCurve_comp_sub 📖	mathematical	—	IsIntegralCurve Real Real.instSub	—	isIntegralCurve_comp_add
isIntegralCurve_const 📖	mathematical	NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	IsIntegralCurve	—	hasDerivAt_const

---

← Back to Index