ImplicitContDiff

📁 Source: Mathlib/Analysis/Calculus/ImplicitContDiff.lean

Statistics

Metric	Count
Definitions implicitFunction, IsContDiffImplicitAt, implicitFunction	3
Theorems contDiffAt_implicitFunction, eventually_apply_eq_iff_implicitFunction, eventually_apply_implicitFunction, hasStrictFDerivAt_implicitFunction, implicitFunction_apply_self, implicitFunction_def, contDiffAt_implicitFunction, apply_implicitFunction, bijective, contDiffAt, contDiffAt_implicitFunction, eventually_implicitFunction_apply_eq, hasFDerivAt, implicitFunction_def, ne_zero	15
Total	18

ContDiffAt

Definitions

Name	Category	Theorems
implicitFunction 📖	CompOp	10 math math: implicitFunction_def, eventually_apply_eq_iff_implicitFunction, IsContDiffImplicitAt.apply_implicitFunction, contDiffAt_implicitFunction, IsContDiffImplicitAt.eventually_implicitFunction_apply_eq, hasStrictFDerivAt_implicitFunction, eventually_apply_implicitFunction, implicitFunction_apply_self, IsContDiffImplicitAt.contDiffAt_implicitFunction, IsContDiffImplicitAt.implicitFunction_def

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contDiffAt_implicitFunction 📖	mathematical	ContDiffAt DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ContinuousLinearMap.IsInvertible UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule DenselyNormedField.toNormedField AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup ContinuousLinearMap.comp RingHom.id Semiring.toNonAssocSemiring instTopologicalSpaceProd Prod.instAddCommGroup Prod.instModule RingHomCompTriple.ids fderiv ContinuousLinearMap.inr	ContDiffAt DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField implicitFunction	—	RingHomCompTriple.ids hasStrictFDerivAt implicitFunction_def CompleteSpace.prod HasStrictFDerivAt.implicitFunctionOfProdDomain_def HasStrictFDerivAt.pt_implicitFunctionDataOfProdDomain ImplicitFunctionData.prodFun_apply HasStrictFDerivAt.leftFun_implicitFunctionDataOfProdDomain HasStrictFDerivAt.rightFun_implicitFunctionDataOfProdDomain ImplicitFunctionData.contDiffAt_implicitFunction contDiffAt_fst snd fun_comp prodMk contDiffAt_const contDiffAt_fun_id
eventually_apply_eq_iff_implicitFunction 📖	mathematical	ContDiffAt DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ContinuousLinearMap.IsInvertible UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule DenselyNormedField.toNormedField AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup ContinuousLinearMap.comp RingHom.id Semiring.toNonAssocSemiring instTopologicalSpaceProd Prod.instAddCommGroup Prod.instModule RingHomCompTriple.ids fderiv ContinuousLinearMap.inr	Filter.Eventually implicitFunction nhds instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	—	RingHomCompTriple.ids HasStrictFDerivAt.eventually_apply_eq_iff_implicitFunctionOfProdDomain hasStrictFDerivAt
eventually_apply_implicitFunction 📖	mathematical	ContDiffAt DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ContinuousLinearMap.IsInvertible UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule DenselyNormedField.toNormedField AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup ContinuousLinearMap.comp RingHom.id Semiring.toNonAssocSemiring instTopologicalSpaceProd Prod.instAddCommGroup Prod.instModule RingHomCompTriple.ids fderiv ContinuousLinearMap.inr	Filter.Eventually implicitFunction nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	—	RingHomCompTriple.ids HasStrictFDerivAt.eventually_apply_implicitFunctionOfProdDomain hasStrictFDerivAt
hasStrictFDerivAt_implicitFunction 📖	mathematical	ContDiffAt DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ContinuousLinearMap.IsInvertible UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule DenselyNormedField.toNormedField AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup ContinuousLinearMap.comp RingHom.id Semiring.toNonAssocSemiring instTopologicalSpaceProd Prod.instAddCommGroup Prod.instModule RingHomCompTriple.ids fderiv ContinuousLinearMap.inr	HasStrictFDerivAt DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule DenselyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace implicitFunction ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousLinearMap.neg NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.comp AddCommGroup.toAddCommMonoid RingHomCompTriple.ids ContinuousLinearMap.inverse instTopologicalSpaceProd Prod.instAddCommGroup Prod.instModule fderiv ContinuousLinearMap.inr ContinuousLinearMap.inl	—	RingHomCompTriple.ids HasStrictFDerivAt.hasStrictFDerivAt_implicitFunctionOfProdDomain hasStrictFDerivAt
implicitFunction_apply_self 📖	mathematical	ContDiffAt DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ContinuousLinearMap.IsInvertible UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule DenselyNormedField.toNormedField AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup ContinuousLinearMap.comp RingHom.id Semiring.toNonAssocSemiring instTopologicalSpaceProd Prod.instAddCommGroup Prod.instModule RingHomCompTriple.ids fderiv ContinuousLinearMap.inr	implicitFunction	—	RingHomCompTriple.ids eq_of_tendsto_nhds T2Space.t1Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace HasStrictFDerivAt.tendsto_implicitFunctionOfProdDomain hasStrictFDerivAt
implicitFunction_def 📖	mathematical	ContDiffAt DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ContinuousLinearMap.IsInvertible UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule DenselyNormedField.toNormedField AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup ContinuousLinearMap.comp RingHom.id Semiring.toNonAssocSemiring instTopologicalSpaceProd Prod.instAddCommGroup Prod.instModule RingHomCompTriple.ids fderiv ContinuousLinearMap.inr	implicitFunction HasStrictFDerivAt.implicitFunctionOfProdDomain DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField fderiv NormedAddCommGroup.toAddCommGroup Prod.normedAddCommGroup NormedSpace.toModule DenselyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace hasStrictFDerivAt	—	RingHomCompTriple.ids

ImplicitFunctionData

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contDiffAt_implicitFunction 📖	mathematical	ContDiffAt DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField leftFun pt rightFun	ContDiffAt DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup implicitFunction prodFun pt	—	CompleteSpace.prod range_leftDeriv range_rightDeriv isCompl_ker hasStrictFDerivAt implicitFunction_def HasStrictFDerivAt.localInverse_def ContDiffAt.to_localInverse prodFun_apply ContDiffAt.prodMk HasStrictFDerivAt.hasFDerivAt RingHomInvPair.ids

IsContDiffImplicitAt

Definitions

Name	Category	Theorems
implicitFunction 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_implicitFunction 📖	mathematical	ContDiffAt DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ContinuousLinearMap.IsInvertible UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule DenselyNormedField.toNormedField AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup ContinuousLinearMap.comp RingHom.id Semiring.toNonAssocSemiring instTopologicalSpaceProd Prod.instAddCommGroup Prod.instModule RingHomCompTriple.ids fderiv ContinuousLinearMap.inr	Filter.Eventually ContDiffAt.implicitFunction nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	—	ContDiffAt.eventually_apply_implicitFunction
bijective 📖	mathematical	IsContDiffImplicitAt	Function.Bijective DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.funLike ContinuousLinearMap.comp instTopologicalSpaceProd Prod.instAddCommMonoid Prod.instModule RingHomCompTriple.ids ContinuousLinearMap.inr	—	—
contDiffAt 📖	mathematical	IsContDiffImplicitAt	ContDiffAt DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup	—	—
contDiffAt_implicitFunction 📖	mathematical	ContDiffAt DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ContinuousLinearMap.IsInvertible UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule DenselyNormedField.toNormedField AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup ContinuousLinearMap.comp RingHom.id Semiring.toNonAssocSemiring instTopologicalSpaceProd Prod.instAddCommGroup Prod.instModule RingHomCompTriple.ids fderiv ContinuousLinearMap.inr	ContDiffAt DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField ContDiffAt.implicitFunction	—	ContDiffAt.contDiffAt_implicitFunction
eventually_implicitFunction_apply_eq 📖	mathematical	ContDiffAt DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ContinuousLinearMap.IsInvertible UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule DenselyNormedField.toNormedField AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup ContinuousLinearMap.comp RingHom.id Semiring.toNonAssocSemiring instTopologicalSpaceProd Prod.instAddCommGroup Prod.instModule RingHomCompTriple.ids fderiv ContinuousLinearMap.inr	Filter.Eventually ContDiffAt.implicitFunction nhds instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	—	ContDiffAt.eventually_apply_eq_iff_implicitFunction
hasFDerivAt 📖	mathematical	IsContDiffImplicitAt	HasFDerivAt DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField Prod.instAddCommGroup NormedAddCommGroup.toAddCommGroup Prod.instModule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule instTopologicalSpaceProd	—	—
implicitFunction_def 📖	mathematical	ContDiffAt DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ContinuousLinearMap.IsInvertible UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule DenselyNormedField.toNormedField AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup ContinuousLinearMap.comp RingHom.id Semiring.toNonAssocSemiring instTopologicalSpaceProd Prod.instAddCommGroup Prod.instModule RingHomCompTriple.ids fderiv ContinuousLinearMap.inr	ContDiffAt.implicitFunction HasStrictFDerivAt.implicitFunctionOfProdDomain DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField fderiv NormedAddCommGroup.toAddCommGroup Prod.normedAddCommGroup NormedSpace.toModule DenselyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContDiffAt.hasStrictFDerivAt	—	ContDiffAt.implicitFunction_def
ne_zero 📖	—	IsContDiffImplicitAt	—	—	—

(root)

Definitions

Name	Category	Theorems
IsContDiffImplicitAt 📖	CompData	—

---

← Back to Index