Implicit

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

Statistics

Metric	Count
Definitions implicitFunction, implicitFunctionDataOfComplemented, implicitFunctionOfComplemented, implicitToOpenPartialHomeomorph, implicitToOpenPartialHomeomorphOfComplemented, implicitToPartialHomeomorph, implicitToPartialHomeomorphOfComplemented, ImplicitFunctionData, implicitFunction, leftDeriv, leftFun, prodFun, pt, rightDeriv, rightFun, toOpenPartialHomeomorph, toPartialHomeomorph	17
Theorems implicitFunction, eq_implicitFunction, eq_implicitFunctionOfComplemented, implicitFunctionOfComplemented_apply_image, implicitFunction_apply_image, implicitToOpenPartialHomeomorphOfComplemented_apply, implicitToOpenPartialHomeomorphOfComplemented_apply_ker, implicitToOpenPartialHomeomorphOfComplemented_fst, implicitToOpenPartialHomeomorphOfComplemented_self, implicitToOpenPartialHomeomorph_apply_ker, implicitToOpenPartialHomeomorph_fst, implicitToOpenPartialHomeomorph_self, implicitToPartialHomeomorphOfComplemented_apply, implicitToPartialHomeomorphOfComplemented_apply_ker, implicitToPartialHomeomorphOfComplemented_fst, implicitToPartialHomeomorphOfComplemented_self, implicitToPartialHomeomorph_apply_ker, implicitToPartialHomeomorph_fst, implicitToPartialHomeomorph_self, map_implicitFunctionOfComplemented_eq, map_implicitFunction_eq, mem_implicitToOpenPartialHomeomorphOfComplemented_source, mem_implicitToOpenPartialHomeomorphOfComplemented_target, mem_implicitToOpenPartialHomeomorph_source, mem_implicitToOpenPartialHomeomorph_target, mem_implicitToPartialHomeomorphOfComplemented_source, mem_implicitToPartialHomeomorphOfComplemented_target, mem_implicitToPartialHomeomorph_source, mem_implicitToPartialHomeomorph_target, tendsto_implicitFunction, to_implicitFunction, to_implicitFunctionOfComplemented, differentiableAt_implicitFunction, eventuallyEq_implicitFunction, fderiv_implicitFunction_apply_eq_iff, hasStrictFDerivAt, hasStrictFDerivAt_implicitFunction_fderiv, hasStrictFDerivAt_leftFun, hasStrictFDerivAt_rightFun, implicitFunction_apply, implicitFunction_apply_image, implicitFunction_hasStrictFDerivAt, isCompl_ker, isInvertible_fderiv_prodFun, leftDeriv_fderiv_implicitFunction, left_map_implicitFunction, map_implicitFunction_nhdsWithin_preimage, map_nhds_eq, map_pt_mem_toOpenPartialHomeomorph_target, map_pt_mem_toPartialHomeomorph_target, prodFun_apply, prod_map_implicitFunction, pt_mem_toOpenPartialHomeomorph_source, pt_mem_toPartialHomeomorph_source, range_leftDeriv, range_rightDeriv, rightDeriv_fderiv_implicitFunction, right_map_implicitFunction, toOpenPartialHomeomorph_apply, toOpenPartialHomeomorph_coe, toPartialHomeomorph_apply, toPartialHomeomorph_coe	62
Total	79

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
implicitFunction 📖	mathematical	HasStrictFDerivAt SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace LinearMap.range DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids ContinuousLinearMap.toLinearMap Top.top Submodule Submodule.instTop Filter.Tendsto nhds SetLike.instMembership Submodule.setLike LinearMap.ker instTopologicalSpaceSubtype Submodule.zero	HasStrictFDerivAt.implicitFunction	—	HasStrictFDerivAt.tendsto_implicitFunction

HasStrictFDerivAt

Definitions

Name	Category	Theorems
implicitFunction 📖	CompOp	6 math math: tendsto_implicitFunction, map_implicitFunction_eq, to_implicitFunction, Filter.Tendsto.implicitFunction, implicitFunction_apply_image, eq_implicitFunction
implicitFunctionDataOfComplemented 📖	CompOp	—
implicitFunctionOfComplemented 📖	CompOp	4 math math: map_implicitFunctionOfComplemented_eq, eq_implicitFunctionOfComplemented, to_implicitFunctionOfComplemented, implicitFunctionOfComplemented_apply_image
implicitToOpenPartialHomeomorph 📖	CompOp	11 math math: implicitToPartialHomeomorph_self, mem_implicitToOpenPartialHomeomorph_target, implicitToOpenPartialHomeomorph_self, implicitToOpenPartialHomeomorph_fst, implicitToOpenPartialHomeomorph_apply_ker, mem_implicitToPartialHomeomorph_source, implicitToPartialHomeomorph_fst, mem_implicitToPartialHomeomorph_target, implicitToPartialHomeomorph_apply_ker, mem_implicitToOpenPartialHomeomorph_source, eq_implicitFunction
implicitToOpenPartialHomeomorphOfComplemented 📖	CompOp	13 math math: implicitToOpenPartialHomeomorphOfComplemented_fst, eq_implicitFunctionOfComplemented, mem_implicitToPartialHomeomorphOfComplemented_target, mem_implicitToOpenPartialHomeomorphOfComplemented_target, implicitToOpenPartialHomeomorphOfComplemented_apply_ker, mem_implicitToOpenPartialHomeomorphOfComplemented_source, implicitToOpenPartialHomeomorphOfComplemented_self, implicitToPartialHomeomorphOfComplemented_self, implicitToPartialHomeomorphOfComplemented_fst, implicitToPartialHomeomorphOfComplemented_apply, mem_implicitToPartialHomeomorphOfComplemented_source, implicitToPartialHomeomorphOfComplemented_apply_ker, implicitToOpenPartialHomeomorphOfComplemented_apply
implicitToPartialHomeomorph 📖	CompOp	—
implicitToPartialHomeomorphOfComplemented 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_implicitFunction 📖	mathematical	HasStrictFDerivAt SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace LinearMap.range DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids ContinuousLinearMap.toLinearMap Top.top Submodule Submodule.instTop	Filter.Eventually implicitFunction SetLike.instMembership Submodule.setLike LinearMap.ker OpenPartialHomeomorph.toFun' instTopologicalSpaceProd instTopologicalSpaceSubtype implicitToOpenPartialHomeomorph nhds	—	RingHomSurjective.ids eq_implicitFunctionOfComplemented
eq_implicitFunctionOfComplemented 📖	mathematical	HasStrictFDerivAt SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace LinearMap.range DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids ContinuousLinearMap.toLinearMap Top.top Submodule Submodule.instTop Submodule.ClosedComplemented NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing LinearMap.ker	Filter.Eventually implicitFunctionOfComplemented SetLike.instMembership Submodule.setLike OpenPartialHomeomorph.toFun' instTopologicalSpaceProd instTopologicalSpaceSubtype implicitToOpenPartialHomeomorphOfComplemented nhds	—	RingHomSurjective.ids ImplicitFunctionData.implicitFunction_apply_image IsScalarTower.left ContinuousLinearMap.completeSpace_ker T2Space.t1Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace
implicitFunctionOfComplemented_apply_image 📖	mathematical	HasStrictFDerivAt SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace LinearMap.range DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids ContinuousLinearMap.toLinearMap Top.top Submodule Submodule.instTop Submodule.ClosedComplemented NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing LinearMap.ker	implicitFunctionOfComplemented SetLike.instMembership Submodule.setLike Submodule.zero	—	RingHomSurjective.ids implicitToOpenPartialHomeomorphOfComplemented_self OpenPartialHomeomorph.left_inv mem_implicitToOpenPartialHomeomorphOfComplemented_source
implicitFunction_apply_image 📖	mathematical	HasStrictFDerivAt SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace LinearMap.range DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids ContinuousLinearMap.toLinearMap Top.top Submodule Submodule.instTop	implicitFunction SetLike.instMembership Submodule.setLike LinearMap.ker Submodule.zero	—	RingHomSurjective.ids implicitFunctionOfComplemented_apply_image
implicitToOpenPartialHomeomorphOfComplemented_apply 📖	mathematical	HasStrictFDerivAt SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace LinearMap.range DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids ContinuousLinearMap.toLinearMap Top.top Submodule Submodule.instTop Submodule.ClosedComplemented NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing LinearMap.ker	OpenPartialHomeomorph.toFun' SetLike.instMembership Submodule.setLike instTopologicalSpaceProd instTopologicalSpaceSubtype implicitToOpenPartialHomeomorphOfComplemented Ring.toSemiring AddCommGroup.toAddCommMonoid DFunLike.coe ContinuousLinearMap Submodule.addCommMonoid Submodule.module ContinuousLinearMap.funLike SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	RingHomSurjective.ids
implicitToOpenPartialHomeomorphOfComplemented_apply_ker 📖	mathematical	HasStrictFDerivAt SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace LinearMap.range DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids ContinuousLinearMap.toLinearMap Top.top Submodule Submodule.instTop Submodule.ClosedComplemented NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing LinearMap.ker	OpenPartialHomeomorph.toFun' SetLike.instMembership Submodule.setLike instTopologicalSpaceProd instTopologicalSpaceSubtype implicitToOpenPartialHomeomorphOfComplemented AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	RingHomSurjective.ids add_sub_cancel_right
implicitToOpenPartialHomeomorphOfComplemented_fst 📖	mathematical	HasStrictFDerivAt SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace LinearMap.range DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids ContinuousLinearMap.toLinearMap Top.top Submodule Submodule.instTop Submodule.ClosedComplemented NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing LinearMap.ker	SetLike.instMembership Submodule.setLike OpenPartialHomeomorph.toFun' instTopologicalSpaceProd instTopologicalSpaceSubtype implicitToOpenPartialHomeomorphOfComplemented	—	RingHomSurjective.ids
implicitToOpenPartialHomeomorphOfComplemented_self 📖	mathematical	HasStrictFDerivAt SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace LinearMap.range DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids ContinuousLinearMap.toLinearMap Top.top Submodule Submodule.instTop Submodule.ClosedComplemented NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing LinearMap.ker	OpenPartialHomeomorph.toFun' SetLike.instMembership Submodule.setLike instTopologicalSpaceProd instTopologicalSpaceSubtype implicitToOpenPartialHomeomorphOfComplemented Submodule.zero	—	RingHomSurjective.ids sub_self map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass
implicitToOpenPartialHomeomorph_apply_ker 📖	mathematical	HasStrictFDerivAt SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace LinearMap.range DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids ContinuousLinearMap.toLinearMap Top.top Submodule Submodule.instTop	OpenPartialHomeomorph.toFun' SetLike.instMembership Submodule.setLike LinearMap.ker instTopologicalSpaceProd instTopologicalSpaceSubtype implicitToOpenPartialHomeomorph AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	RingHomSurjective.ids implicitToOpenPartialHomeomorphOfComplemented_apply_ker
implicitToOpenPartialHomeomorph_fst 📖	mathematical	HasStrictFDerivAt SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace LinearMap.range DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids ContinuousLinearMap.toLinearMap Top.top Submodule Submodule.instTop	SetLike.instMembership Submodule.setLike LinearMap.ker OpenPartialHomeomorph.toFun' instTopologicalSpaceProd instTopologicalSpaceSubtype implicitToOpenPartialHomeomorph	—	RingHomSurjective.ids
implicitToOpenPartialHomeomorph_self 📖	mathematical	HasStrictFDerivAt SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace LinearMap.range DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids ContinuousLinearMap.toLinearMap Top.top Submodule Submodule.instTop	OpenPartialHomeomorph.toFun' SetLike.instMembership Submodule.setLike LinearMap.ker instTopologicalSpaceProd instTopologicalSpaceSubtype implicitToOpenPartialHomeomorph Submodule.zero	—	RingHomSurjective.ids implicitToOpenPartialHomeomorphOfComplemented_self
implicitToPartialHomeomorphOfComplemented_apply 📖	mathematical	HasStrictFDerivAt SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace LinearMap.range DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids ContinuousLinearMap.toLinearMap Top.top Submodule Submodule.instTop Submodule.ClosedComplemented NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing LinearMap.ker	OpenPartialHomeomorph.toFun' SetLike.instMembership Submodule.setLike instTopologicalSpaceProd instTopologicalSpaceSubtype implicitToOpenPartialHomeomorphOfComplemented Ring.toSemiring AddCommGroup.toAddCommMonoid DFunLike.coe ContinuousLinearMap Submodule.addCommMonoid Submodule.module ContinuousLinearMap.funLike SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	implicitToOpenPartialHomeomorphOfComplemented_apply
implicitToPartialHomeomorphOfComplemented_apply_ker 📖	mathematical	HasStrictFDerivAt SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace LinearMap.range DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids ContinuousLinearMap.toLinearMap Top.top Submodule Submodule.instTop Submodule.ClosedComplemented NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing LinearMap.ker	OpenPartialHomeomorph.toFun' SetLike.instMembership Submodule.setLike instTopologicalSpaceProd instTopologicalSpaceSubtype implicitToOpenPartialHomeomorphOfComplemented AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	implicitToOpenPartialHomeomorphOfComplemented_apply_ker
implicitToPartialHomeomorphOfComplemented_fst 📖	mathematical	HasStrictFDerivAt SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace LinearMap.range DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids ContinuousLinearMap.toLinearMap Top.top Submodule Submodule.instTop Submodule.ClosedComplemented NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing LinearMap.ker	SetLike.instMembership Submodule.setLike OpenPartialHomeomorph.toFun' instTopologicalSpaceProd instTopologicalSpaceSubtype implicitToOpenPartialHomeomorphOfComplemented	—	implicitToOpenPartialHomeomorphOfComplemented_fst
implicitToPartialHomeomorphOfComplemented_self 📖	mathematical	HasStrictFDerivAt SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace LinearMap.range DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids ContinuousLinearMap.toLinearMap Top.top Submodule Submodule.instTop Submodule.ClosedComplemented NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing LinearMap.ker	OpenPartialHomeomorph.toFun' SetLike.instMembership Submodule.setLike instTopologicalSpaceProd instTopologicalSpaceSubtype implicitToOpenPartialHomeomorphOfComplemented Submodule.zero	—	implicitToOpenPartialHomeomorphOfComplemented_self
implicitToPartialHomeomorph_apply_ker 📖	mathematical	HasStrictFDerivAt SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace LinearMap.range DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids ContinuousLinearMap.toLinearMap Top.top Submodule Submodule.instTop	OpenPartialHomeomorph.toFun' SetLike.instMembership Submodule.setLike LinearMap.ker instTopologicalSpaceProd instTopologicalSpaceSubtype implicitToOpenPartialHomeomorph AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	implicitToOpenPartialHomeomorph_apply_ker
implicitToPartialHomeomorph_fst 📖	mathematical	HasStrictFDerivAt SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace LinearMap.range DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids ContinuousLinearMap.toLinearMap Top.top Submodule Submodule.instTop	SetLike.instMembership Submodule.setLike LinearMap.ker OpenPartialHomeomorph.toFun' instTopologicalSpaceProd instTopologicalSpaceSubtype implicitToOpenPartialHomeomorph	—	implicitToOpenPartialHomeomorph_fst
implicitToPartialHomeomorph_self 📖	mathematical	HasStrictFDerivAt SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace LinearMap.range DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids ContinuousLinearMap.toLinearMap Top.top Submodule Submodule.instTop	OpenPartialHomeomorph.toFun' SetLike.instMembership Submodule.setLike LinearMap.ker instTopologicalSpaceProd instTopologicalSpaceSubtype implicitToOpenPartialHomeomorph Submodule.zero	—	implicitToOpenPartialHomeomorph_self
map_implicitFunctionOfComplemented_eq 📖	mathematical	HasStrictFDerivAt SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace LinearMap.range DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids ContinuousLinearMap.toLinearMap Top.top Submodule Submodule.instTop Submodule.ClosedComplemented NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing LinearMap.ker	Filter.Eventually SetLike.instMembership Submodule.setLike implicitFunctionOfComplemented nhds instTopologicalSpaceProd instTopologicalSpaceSubtype Submodule.zero	—	RingHomSurjective.ids Filter.Eventually.mono OpenPartialHomeomorph.eventually_right_inverse mem_implicitToOpenPartialHomeomorphOfComplemented_target
map_implicitFunction_eq 📖	mathematical	HasStrictFDerivAt SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace LinearMap.range DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids ContinuousLinearMap.toLinearMap Top.top Submodule Submodule.instTop	Filter.Eventually SetLike.instMembership Submodule.setLike LinearMap.ker implicitFunction nhds instTopologicalSpaceProd instTopologicalSpaceSubtype Submodule.zero	—	RingHomSurjective.ids map_implicitFunctionOfComplemented_eq
mem_implicitToOpenPartialHomeomorphOfComplemented_source 📖	mathematical	HasStrictFDerivAt SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace LinearMap.range DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids ContinuousLinearMap.toLinearMap Top.top Submodule Submodule.instTop Submodule.ClosedComplemented NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing LinearMap.ker	Set Set.instMembership PartialEquiv.source SetLike.instMembership Submodule.setLike OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd instTopologicalSpaceSubtype implicitToOpenPartialHomeomorphOfComplemented	—	RingHomSurjective.ids ImplicitFunctionData.pt_mem_toOpenPartialHomeomorph_source
mem_implicitToOpenPartialHomeomorphOfComplemented_target 📖	mathematical	HasStrictFDerivAt SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace LinearMap.range DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids ContinuousLinearMap.toLinearMap Top.top Submodule Submodule.instTop Submodule.ClosedComplemented NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing LinearMap.ker	SetLike.instMembership Submodule.setLike Set Set.instMembership PartialEquiv.target OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd instTopologicalSpaceSubtype implicitToOpenPartialHomeomorphOfComplemented Submodule.zero	—	RingHomSurjective.ids implicitToOpenPartialHomeomorphOfComplemented_self OpenPartialHomeomorph.map_source mem_implicitToOpenPartialHomeomorphOfComplemented_source
mem_implicitToOpenPartialHomeomorph_source 📖	mathematical	HasStrictFDerivAt SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace LinearMap.range DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids ContinuousLinearMap.toLinearMap Top.top Submodule Submodule.instTop	Set Set.instMembership PartialEquiv.source SetLike.instMembership Submodule.setLike LinearMap.ker OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd instTopologicalSpaceSubtype implicitToOpenPartialHomeomorph	—	RingHomSurjective.ids ImplicitFunctionData.pt_mem_toOpenPartialHomeomorph_source
mem_implicitToOpenPartialHomeomorph_target 📖	mathematical	HasStrictFDerivAt SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace LinearMap.range DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids ContinuousLinearMap.toLinearMap Top.top Submodule Submodule.instTop	SetLike.instMembership Submodule.setLike LinearMap.ker Set Set.instMembership PartialEquiv.target OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd instTopologicalSpaceSubtype implicitToOpenPartialHomeomorph Submodule.zero	—	RingHomSurjective.ids mem_implicitToOpenPartialHomeomorphOfComplemented_target
mem_implicitToPartialHomeomorphOfComplemented_source 📖	mathematical	HasStrictFDerivAt SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace LinearMap.range DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids ContinuousLinearMap.toLinearMap Top.top Submodule Submodule.instTop Submodule.ClosedComplemented NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing LinearMap.ker	Set Set.instMembership PartialEquiv.source SetLike.instMembership Submodule.setLike OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd instTopologicalSpaceSubtype implicitToOpenPartialHomeomorphOfComplemented	—	mem_implicitToOpenPartialHomeomorphOfComplemented_source
mem_implicitToPartialHomeomorphOfComplemented_target 📖	mathematical	HasStrictFDerivAt SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace LinearMap.range DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids ContinuousLinearMap.toLinearMap Top.top Submodule Submodule.instTop Submodule.ClosedComplemented NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing LinearMap.ker	SetLike.instMembership Submodule.setLike Set Set.instMembership PartialEquiv.target OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd instTopologicalSpaceSubtype implicitToOpenPartialHomeomorphOfComplemented Submodule.zero	—	mem_implicitToOpenPartialHomeomorphOfComplemented_target
mem_implicitToPartialHomeomorph_source 📖	mathematical	HasStrictFDerivAt SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace LinearMap.range DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids ContinuousLinearMap.toLinearMap Top.top Submodule Submodule.instTop	Set Set.instMembership PartialEquiv.source SetLike.instMembership Submodule.setLike LinearMap.ker OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd instTopologicalSpaceSubtype implicitToOpenPartialHomeomorph	—	mem_implicitToOpenPartialHomeomorph_source
mem_implicitToPartialHomeomorph_target 📖	mathematical	HasStrictFDerivAt SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace LinearMap.range DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids ContinuousLinearMap.toLinearMap Top.top Submodule Submodule.instTop	SetLike.instMembership Submodule.setLike LinearMap.ker Set Set.instMembership PartialEquiv.target OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd instTopologicalSpaceSubtype implicitToOpenPartialHomeomorph Submodule.zero	—	mem_implicitToOpenPartialHomeomorph_target
tendsto_implicitFunction 📖	mathematical	HasStrictFDerivAt SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace LinearMap.range DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids ContinuousLinearMap.toLinearMap Top.top Submodule Submodule.instTop Filter.Tendsto nhds SetLike.instMembership Submodule.setLike LinearMap.ker instTopologicalSpaceSubtype Submodule.zero	implicitFunction	—	RingHomSurjective.ids Filter.Tendsto.comp OpenPartialHomeomorph.tendsto_symm mem_implicitToOpenPartialHomeomorph_source implicitToOpenPartialHomeomorph_self Filter.Tendsto.prodMk_nhds
to_implicitFunction 📖	mathematical	HasStrictFDerivAt SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace LinearMap.range DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids ContinuousLinearMap.toLinearMap Top.top Submodule Submodule.instTop	SetLike.instMembership Submodule.setLike LinearMap.ker Submodule.addCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Submodule.module instTopologicalSpaceSubtype implicitFunction Submodule.subtypeL Submodule.zero	—	RingHomSurjective.ids to_implicitFunctionOfComplemented
to_implicitFunctionOfComplemented 📖	mathematical	HasStrictFDerivAt SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace LinearMap.range DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids ContinuousLinearMap.toLinearMap Top.top Submodule Submodule.instTop Submodule.ClosedComplemented NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing LinearMap.ker	SetLike.instMembership Submodule.setLike Submodule.addCommGroup Submodule.module instTopologicalSpaceSubtype implicitFunctionOfComplemented Submodule.subtypeL Submodule.zero	—	RingHomSurjective.ids IsScalarTower.left ContinuousLinearMap.completeSpace_ker T2Space.t1Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass sub_self ImplicitFunctionData.implicitFunction_hasStrictFDerivAt ContinuousLinearMap.ext RingHomCompTriple.ids ContinuousLinearMap.apply_val_ker

ImplicitFunctionData

Definitions

Name	Category	Theorems
implicitFunction 📖	CompOp	16 math math: implicitFunction_hasStrictFDerivAt, eventuallyEq_implicitFunction, leftDeriv_fderiv_implicitFunction, hasStrictFDerivAt_implicitFunction_fderiv, IsContDiffImplicitAt.implicitFunction_apply, implicitFunction_apply, differentiableAt_implicitFunction, fderiv_implicitFunction_apply_eq_iff, implicitFunction_apply_image, contDiff_implicitFunction, right_map_implicitFunction, prod_map_implicitFunction, IsContDiffImplicitAt.implicitFunction_def, map_implicitFunction_nhdsWithin_preimage, rightDeriv_fderiv_implicitFunction, left_map_implicitFunction
leftDeriv 📖	CompOp	6 math math: isCompl_ker, hasStrictFDerivAt_leftFun, range_leftDeriv, leftDeriv_fderiv_implicitFunction, hasStrictFDerivAt, fderiv_implicitFunction_apply_eq_iff
leftFun 📖	CompOp	18 math math: hasStrictFDerivAt_leftFun, map_pt_mem_toOpenPartialHomeomorph_target, implicitFunction_hasStrictFDerivAt, map_pt_mem_toPartialHomeomorph_target, leftDeriv_fderiv_implicitFunction, hasStrictFDerivAt_implicitFunction_fderiv, map_nhds_eq, prodFun_apply, differentiableAt_implicitFunction, fderiv_implicitFunction_apply_eq_iff, implicitFunction_apply_image, IsContDiffImplicitAt.implicitFunctionData_leftFun_apply, toPartialHomeomorph_apply, toOpenPartialHomeomorph_apply, map_implicitFunction_nhdsWithin_preimage, rightDeriv_fderiv_implicitFunction, left_map_implicitFunction, IsContDiffImplicitAt.implicitFunctionData_leftFun_pt
prodFun 📖	CompOp	10 math math: isInvertible_fderiv_prodFun, eventuallyEq_implicitFunction, prodFun_apply, toPartialHomeomorph_coe, hasStrictFDerivAt, contDiff_implicitFunction, right_map_implicitFunction, toOpenPartialHomeomorph_coe, prod_map_implicitFunction, left_map_implicitFunction
pt 📖	CompOp	23 math math: isInvertible_fderiv_prodFun, hasStrictFDerivAt_leftFun, map_pt_mem_toOpenPartialHomeomorph_target, pt_mem_toPartialHomeomorph_source, implicitFunction_hasStrictFDerivAt, map_pt_mem_toPartialHomeomorph_target, pt_mem_toOpenPartialHomeomorph_source, leftDeriv_fderiv_implicitFunction, hasStrictFDerivAt_implicitFunction_fderiv, map_nhds_eq, IsContDiffImplicitAt.implicitFunctionData_pt, differentiableAt_implicitFunction, hasStrictFDerivAt, fderiv_implicitFunction_apply_eq_iff, implicitFunction_apply_image, IsContDiffImplicitAt.implicitFunctionData_rightFun_pt, right_map_implicitFunction, prod_map_implicitFunction, map_implicitFunction_nhdsWithin_preimage, rightDeriv_fderiv_implicitFunction, hasStrictFDerivAt_rightFun, left_map_implicitFunction, IsContDiffImplicitAt.implicitFunctionData_leftFun_pt
rightDeriv 📖	CompOp	6 math math: isCompl_ker, hasStrictFDerivAt, fderiv_implicitFunction_apply_eq_iff, range_rightDeriv, rightDeriv_fderiv_implicitFunction, hasStrictFDerivAt_rightFun
rightFun 📖	CompOp	17 math math: map_pt_mem_toOpenPartialHomeomorph_target, implicitFunction_hasStrictFDerivAt, map_pt_mem_toPartialHomeomorph_target, leftDeriv_fderiv_implicitFunction, hasStrictFDerivAt_implicitFunction_fderiv, prodFun_apply, differentiableAt_implicitFunction, IsContDiffImplicitAt.implicitFunctionData_rightFun_apply, fderiv_implicitFunction_apply_eq_iff, implicitFunction_apply_image, IsContDiffImplicitAt.implicitFunctionData_rightFun_pt, right_map_implicitFunction, toPartialHomeomorph_apply, toOpenPartialHomeomorph_apply, map_implicitFunction_nhdsWithin_preimage, rightDeriv_fderiv_implicitFunction, hasStrictFDerivAt_rightFun
toOpenPartialHomeomorph 📖	CompOp	9 math math: map_pt_mem_toOpenPartialHomeomorph_target, pt_mem_toPartialHomeomorph_source, map_pt_mem_toPartialHomeomorph_target, pt_mem_toOpenPartialHomeomorph_source, toPartialHomeomorph_coe, implicitFunction_apply, toOpenPartialHomeomorph_coe, toPartialHomeomorph_apply, toOpenPartialHomeomorph_apply
toPartialHomeomorph 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
differentiableAt_implicitFunction 📖	mathematical	—	DifferentiableAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace implicitFunction leftFun pt rightFun	—	HasFDerivAt.differentiableAt HasStrictFDerivAt.hasFDerivAt hasStrictFDerivAt_implicitFunction_fderiv
eventuallyEq_implicitFunction 📖	mathematical	Filter.Eventually leftFun rightFun nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup pt	Filter.EventuallyEq instTopologicalSpaceProd prodFun implicitFunction	—	HasStrictFDerivAt.localInverse_unique range_leftDeriv range_rightDeriv isCompl_ker hasStrictFDerivAt
fderiv_implicitFunction_apply_eq_iff 📖	mathematical	—	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toModule ContinuousLinearMap.funLike fderiv implicitFunction leftFun pt rightFun ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid leftDeriv NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid rightDeriv	—	range_leftDeriv range_rightDeriv isCompl_ker hasStrictFDerivAt RingHomCompTriple.ids RingHomInvPair.ids CompleteSpace.prod HasFDerivAt.fderiv IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace HasStrictFDerivAt.hasFDerivAt HasStrictFDerivAt.comp HasStrictFDerivAt.to_localInverse HasStrictFDerivAt.prodMk hasStrictFDerivAt_const hasStrictFDerivAt_id
hasStrictFDerivAt 📖	mathematical	—	HasStrictFDerivAt SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Prod.instAddCommGroup NormedAddCommGroup.toAddCommGroup Prod.instModule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instTopologicalSpaceProd prodFun ContinuousLinearEquiv.toContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Prod.instAddCommMonoid ContinuousLinearMap.equivProdOfSurjectiveOfIsCompl CompleteSpace.prod leftDeriv rightDeriv range_leftDeriv range_rightDeriv isCompl_ker pt	—	HasStrictFDerivAt.prodMk hasStrictFDerivAt_leftFun hasStrictFDerivAt_rightFun
hasStrictFDerivAt_implicitFunction_fderiv 📖	mathematical	—	HasStrictFDerivAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace implicitFunction leftFun pt fderiv rightFun	—	CompleteSpace.prod range_leftDeriv range_rightDeriv isCompl_ker hasStrictFDerivAt RingHomCompTriple.ids RingHomInvPair.ids HasStrictFDerivAt.comp HasStrictFDerivAt.to_localInverse HasStrictFDerivAt.prodMk hasStrictFDerivAt_const hasStrictFDerivAt_id HasFDerivAt.fderiv IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace HasStrictFDerivAt.hasFDerivAt
hasStrictFDerivAt_leftFun 📖	mathematical	—	HasStrictFDerivAt SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace leftFun leftDeriv pt	—	—
hasStrictFDerivAt_rightFun 📖	mathematical	—	HasStrictFDerivAt SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace rightFun rightDeriv pt	—	—
implicitFunction_apply 📖	mathematical	—	implicitFunction OpenPartialHomeomorph.toFun' instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup OpenPartialHomeomorph.symm toOpenPartialHomeomorph	—	—
implicitFunction_apply_image 📖	mathematical	—	Filter.Eventually implicitFunction leftFun rightFun nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup pt	—	HasStrictFDerivAt.eventually_left_inverse CompleteSpace.prod range_leftDeriv range_rightDeriv isCompl_ker hasStrictFDerivAt
implicitFunction_hasStrictFDerivAt 📖	mathematical	ContinuousLinearMap.comp DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule RingHomCompTriple.ids rightDeriv ContinuousLinearMap.id leftDeriv ContinuousLinearMap ContinuousLinearMap.zero	HasStrictFDerivAt SeminormedAddCommGroup.toAddCommGroup implicitFunction leftFun pt rightFun	—	RingHomCompTriple.ids ContinuousLinearMap.ext fderiv_implicitFunction_apply_eq_iff hasStrictFDerivAt_implicitFunction_fderiv
isCompl_ker 📖	mathematical	—	IsCompl Submodule 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 Submodule.instPartialOrder CompleteLattice.toBoundedOrder Submodule.completeLattice LinearMap.ker RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.toLinearMap leftDeriv rightDeriv	—	—
isInvertible_fderiv_prodFun 📖	mathematical	—	ContinuousLinearMap.IsInvertible UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup instTopologicalSpaceProd DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Prod.instAddCommGroup Prod.instModule ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid fderiv prodFun pt	—	RingHomInvPair.ids CompleteSpace.prod range_leftDeriv range_rightDeriv isCompl_ker HasFDerivAt.fderiv IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Prod.continuousAdd Prod.continuousSMul Prod.t2Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace HasStrictFDerivAt.hasFDerivAt hasStrictFDerivAt ContinuousLinearMap.isInvertible_equiv
leftDeriv_fderiv_implicitFunction 📖	mathematical	—	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.funLike leftDeriv AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup fderiv implicitFunction leftFun pt rightFun NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	fderiv_implicitFunction_apply_eq_iff
left_map_implicitFunction 📖	mathematical	—	Filter.Eventually leftFun implicitFunction nhds instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup prodFun pt	—	Filter.Eventually.mono prod_map_implicitFunction
map_implicitFunction_nhdsWithin_preimage 📖	mathematical	—	Filter.map implicitFunction leftFun pt nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup rightFun Set.preimage Set Set.instInter Set.instSingletonSet	—	Filter.map_map Topology.IsInducing.map_nhdsWithin_eq isInducing_prodMkRight Set.singleton_prod OpenPartialHomeomorph.map_nhdsWithin_eq OpenPartialHomeomorph.mapsTo pt_mem_toOpenPartialHomeomorph_source prodFun_apply toOpenPartialHomeomorph_coe OpenPartialHomeomorph.leftInvOn OpenPartialHomeomorph.image_source_inter_eq' OpenPartialHomeomorph.nhdsWithin_source_inter Set.ext
map_nhds_eq 📖	mathematical	—	Filter.map leftFun nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup pt	—	Filter.map_map HasStrictFDerivAt.map_nhds_eq_of_equiv CompleteSpace.prod range_leftDeriv range_rightDeriv isCompl_ker hasStrictFDerivAt map_fst_nhds
map_pt_mem_toOpenPartialHomeomorph_target 📖	mathematical	—	Set Set.instMembership PartialEquiv.target OpenPartialHomeomorph.toPartialEquiv UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup instTopologicalSpaceProd toOpenPartialHomeomorph leftFun pt rightFun	—	OpenPartialHomeomorph.map_source pt_mem_toOpenPartialHomeomorph_source
map_pt_mem_toPartialHomeomorph_target 📖	mathematical	—	Set Set.instMembership PartialEquiv.target OpenPartialHomeomorph.toPartialEquiv UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup instTopologicalSpaceProd toOpenPartialHomeomorph leftFun pt rightFun	—	map_pt_mem_toOpenPartialHomeomorph_target
prodFun_apply 📖	mathematical	—	prodFun leftFun rightFun	—	—
prod_map_implicitFunction 📖	mathematical	—	Filter.Eventually prodFun implicitFunction nhds instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup pt	—	Filter.Eventually.mono CompleteSpace.prod range_leftDeriv range_rightDeriv isCompl_ker hasStrictFDerivAt HasStrictFDerivAt.eventually_right_inverse
pt_mem_toOpenPartialHomeomorph_source 📖	mathematical	—	Set Set.instMembership PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup instTopologicalSpaceProd toOpenPartialHomeomorph pt	—	HasStrictFDerivAt.mem_toOpenPartialHomeomorph_source CompleteSpace.prod range_leftDeriv range_rightDeriv isCompl_ker hasStrictFDerivAt
pt_mem_toPartialHomeomorph_source 📖	mathematical	—	Set Set.instMembership PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup instTopologicalSpaceProd toOpenPartialHomeomorph pt	—	pt_mem_toOpenPartialHomeomorph_source
range_leftDeriv 📖	mathematical	—	LinearMap.range 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 RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids ContinuousLinearMap.toLinearMap leftDeriv Top.top Submodule Submodule.instTop	—	—
range_rightDeriv 📖	mathematical	—	LinearMap.range 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 RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids ContinuousLinearMap.toLinearMap rightDeriv Top.top Submodule Submodule.instTop	—	—
rightDeriv_fderiv_implicitFunction 📖	mathematical	—	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.funLike rightDeriv AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup fderiv implicitFunction leftFun pt rightFun	—	fderiv_implicitFunction_apply_eq_iff
right_map_implicitFunction 📖	mathematical	—	Filter.Eventually rightFun implicitFunction nhds instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup prodFun pt	—	Filter.Eventually.mono prod_map_implicitFunction
toOpenPartialHomeomorph_apply 📖	mathematical	—	OpenPartialHomeomorph.toFun' UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup instTopologicalSpaceProd toOpenPartialHomeomorph leftFun rightFun	—	—
toOpenPartialHomeomorph_coe 📖	mathematical	—	OpenPartialHomeomorph.toFun' UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup instTopologicalSpaceProd toOpenPartialHomeomorph prodFun	—	—
toPartialHomeomorph_apply 📖	mathematical	—	OpenPartialHomeomorph.toFun' UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup instTopologicalSpaceProd toOpenPartialHomeomorph leftFun rightFun	—	toOpenPartialHomeomorph_apply
toPartialHomeomorph_coe 📖	mathematical	—	OpenPartialHomeomorph.toFun' UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup instTopologicalSpaceProd toOpenPartialHomeomorph prodFun	—	toOpenPartialHomeomorph_coe

(root)

Definitions

Name	Category	Theorems
ImplicitFunctionData 📖	CompData	—

---

← Back to Index