ProdDomain

📁 Source: Mathlib/Analysis/Calculus/ImplicitFunction/ProdDomain.lean

Statistics

Metric	Count
Definitions implicitFunctionDataOfProdDomain, implicitFunctionOfProdDomain	2
Theorems eventually_apply_eq_iff_implicitFunctionOfProdDomain, eventually_apply_implicitFunctionOfProdDomain, hasStrictFDerivAt_implicitFunctionOfProdDomain, implicitFunctionOfProdDomain_def, leftFun_implicitFunctionDataOfProdDomain, pt_implicitFunctionDataOfProdDomain, rightFun_implicitFunctionDataOfProdDomain, tendsto_implicitFunctionOfProdDomain	8
Total	10

HasStrictFDerivAt

Definitions

Name	Category	Theorems
implicitFunctionDataOfProdDomain 📖	CompOp	4 math math: rightFun_implicitFunctionDataOfProdDomain, leftFun_implicitFunctionDataOfProdDomain, pt_implicitFunctionDataOfProdDomain, implicitFunctionOfProdDomain_def
implicitFunctionOfProdDomain 📖	CompOp	7 math math: ContDiffAt.implicitFunction_def, eventually_apply_eq_iff_implicitFunctionOfProdDomain, hasStrictFDerivAt_implicitFunctionOfProdDomain, tendsto_implicitFunctionOfProdDomain, eventually_apply_implicitFunctionOfProdDomain, IsContDiffImplicitAt.implicitFunction_def, implicitFunctionOfProdDomain_def

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eventually_apply_eq_iff_implicitFunctionOfProdDomain 📖	mathematical	HasStrictFDerivAt Prod.instAddCommGroup NormedAddCommGroup.toAddCommGroup Prod.instModule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule instTopologicalSpaceProd ContinuousLinearMap.IsInvertible ContinuousLinearMap.comp RingHom.id Semiring.toNonAssocSemiring Prod.instAddCommMonoid RingHomCompTriple.ids ContinuousLinearMap.inr	Filter.Eventually implicitFunctionOfProdDomain nhds instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	—	RingHomCompTriple.ids CompleteSpace.prod Filter.mp_mem ImplicitFunctionData.rightFun_implicitFunction_eq_rightFun ImplicitFunctionData.leftFun_eq_iff_implicitFunction Filter.univ_mem' pt_implicitFunctionDataOfProdDomain leftFun_implicitFunctionDataOfProdDomain rightFun_implicitFunctionDataOfProdDomain
eventually_apply_implicitFunctionOfProdDomain 📖	mathematical	HasStrictFDerivAt Prod.instAddCommGroup NormedAddCommGroup.toAddCommGroup Prod.instModule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule instTopologicalSpaceProd ContinuousLinearMap.IsInvertible ContinuousLinearMap.comp RingHom.id Semiring.toNonAssocSemiring Prod.instAddCommMonoid RingHomCompTriple.ids ContinuousLinearMap.inr	Filter.Eventually implicitFunctionOfProdDomain nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	—	RingHomCompTriple.ids tendsto_implicitFunctionOfProdDomain Filter.Eventually.image_of_prod nhds_prod_eq eventually_apply_eq_iff_implicitFunctionOfProdDomain
hasStrictFDerivAt_implicitFunctionOfProdDomain 📖	mathematical	HasStrictFDerivAt Prod.instAddCommGroup NormedAddCommGroup.toAddCommGroup Prod.instModule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule instTopologicalSpaceProd ContinuousLinearMap.IsInvertible ContinuousLinearMap.comp RingHom.id Semiring.toNonAssocSemiring Prod.instAddCommMonoid RingHomCompTriple.ids ContinuousLinearMap.inr	HasStrictFDerivAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace implicitFunctionOfProdDomain ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousLinearMap.neg NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.comp RingHomCompTriple.ids ContinuousLinearMap.inverse instTopologicalSpaceProd Prod.instAddCommMonoid Prod.instModule ContinuousLinearMap.inr ContinuousLinearMap.inl	—	RingHomCompTriple.ids SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.ext ContinuousLinearMap.comp_apply ContinuousLinearMap.comp_inl_add_comp_inr map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass ContinuousLinearMap.IsInvertible.self_apply_inverse add_neg_cancel snd CompleteSpace.prod ImplicitFunctionData.hasStrictFDerivAt_implicitFunction ContinuousLinearMap.fst_comp_prod
implicitFunctionOfProdDomain_def 📖	mathematical	HasStrictFDerivAt Prod.instAddCommGroup NormedAddCommGroup.toAddCommGroup Prod.instModule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule instTopologicalSpaceProd ContinuousLinearMap.IsInvertible ContinuousLinearMap.comp RingHom.id Semiring.toNonAssocSemiring Prod.instAddCommMonoid RingHomCompTriple.ids ContinuousLinearMap.inr	implicitFunctionOfProdDomain ImplicitFunctionData.implicitFunction Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup CompleteSpace.prod PseudoEMetricSpace.toUniformSpace PseudoMetricSpace.toPseudoEMetricSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup implicitFunctionDataOfProdDomain	—	RingHomCompTriple.ids
leftFun_implicitFunctionDataOfProdDomain 📖	mathematical	HasStrictFDerivAt Prod.instAddCommGroup NormedAddCommGroup.toAddCommGroup Prod.instModule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule instTopologicalSpaceProd ContinuousLinearMap.IsInvertible ContinuousLinearMap.comp RingHom.id Semiring.toNonAssocSemiring Prod.instAddCommMonoid RingHomCompTriple.ids ContinuousLinearMap.inr	ImplicitFunctionData.leftFun Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup CompleteSpace.prod PseudoEMetricSpace.toUniformSpace PseudoMetricSpace.toPseudoEMetricSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup implicitFunctionDataOfProdDomain	—	RingHomCompTriple.ids CompleteSpace.prod
pt_implicitFunctionDataOfProdDomain 📖	mathematical	HasStrictFDerivAt Prod.instAddCommGroup NormedAddCommGroup.toAddCommGroup Prod.instModule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule instTopologicalSpaceProd ContinuousLinearMap.IsInvertible ContinuousLinearMap.comp RingHom.id Semiring.toNonAssocSemiring Prod.instAddCommMonoid RingHomCompTriple.ids ContinuousLinearMap.inr	ImplicitFunctionData.pt Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup CompleteSpace.prod PseudoEMetricSpace.toUniformSpace PseudoMetricSpace.toPseudoEMetricSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup implicitFunctionDataOfProdDomain	—	RingHomCompTriple.ids CompleteSpace.prod
rightFun_implicitFunctionDataOfProdDomain 📖	mathematical	HasStrictFDerivAt Prod.instAddCommGroup NormedAddCommGroup.toAddCommGroup Prod.instModule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule instTopologicalSpaceProd ContinuousLinearMap.IsInvertible ContinuousLinearMap.comp RingHom.id Semiring.toNonAssocSemiring Prod.instAddCommMonoid RingHomCompTriple.ids ContinuousLinearMap.inr	ImplicitFunctionData.rightFun Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup CompleteSpace.prod PseudoEMetricSpace.toUniformSpace PseudoMetricSpace.toPseudoEMetricSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup implicitFunctionDataOfProdDomain	—	RingHomCompTriple.ids CompleteSpace.prod
tendsto_implicitFunctionOfProdDomain 📖	mathematical	HasStrictFDerivAt Prod.instAddCommGroup NormedAddCommGroup.toAddCommGroup Prod.instModule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule instTopologicalSpaceProd ContinuousLinearMap.IsInvertible ContinuousLinearMap.comp RingHom.id Semiring.toNonAssocSemiring Prod.instAddCommMonoid RingHomCompTriple.ids ContinuousLinearMap.inr	Filter.Tendsto implicitFunctionOfProdDomain nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	—	RingHomCompTriple.ids ContinuousAt.tendsto continuousAt SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul hasStrictFDerivAt_implicitFunctionOfProdDomain Filter.Eventually.self_of_nhds eventually_apply_eq_iff_implicitFunctionOfProdDomain

---

← Back to Index