Documentation Verification Report

ImplicitContDiff

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

Statistics

Metric	Count
Definitions `IsContDiffImplicitAt`, `implicitFunction`, `implicitFunctionAux`, `implicitFunctionData`	4
Theorems `contDiff_implicitFunction`, `apply_implicitFunction`, `bijective`, `comp_implicitFunctionAux_eq_snd`, `contDiffAt`, `contDiffAt_implicitFunction`, `eventually_implicitFunction_apply_eq`, `hasFDerivAt`, `implicitFunctionAux_fst`, `implicitFunctionData_leftFun_apply`, `implicitFunctionData_leftFun_pt`, `implicitFunctionData_pt`, `implicitFunctionData_rightFun_apply`, `implicitFunctionData_rightFun_pt`, `implicitFunction_apply`, `implicitFunction_def`, `ne_zero`, `one_le`	18
Total	22

ImplicitFunctionData

Theorems

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

IsContDiffImplicitAt

Definitions

Name	Category	Theorems
`implicitFunction` 📖	CompOp	4 math math: `apply_implicitFunction`, `implicitFunction_apply`, `contDiffAt_implicitFunction`, `implicitFunction_def`
`implicitFunctionAux` 📖	CompOp	2 math math: `comp_implicitFunctionAux_eq_snd`, `implicitFunctionAux_fst`
`implicitFunctionData` 📖	CompOp	7 math math: `implicitFunction_apply`, `implicitFunctionData_pt`, `implicitFunctionData_rightFun_apply`, `implicitFunctionData_rightFun_pt`, `implicitFunctionData_leftFun_apply`, `implicitFunction_def`, `implicitFunctionData_leftFun_pt`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_implicitFunction` 📖	mathematical	`IsContDiffImplicitAt`	`Filter.Eventually` `implicitFunction` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`comp_implicitFunctionAux_eq_snd` `implicitFunctionAux_fst` `Filter.Eventually.mp` `Filter.Eventually.self_of_nhds` `Filter.Eventually.curry` `Filter.eventually_swap_iff` `nhds_prod_eq` `Filter.Eventually.mono`
`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`	—	—
`comp_implicitFunctionAux_eq_snd` 📖	mathematical	`IsContDiffImplicitAt`	`Filter.Eventually` `implicitFunctionAux` `nhds` `instTopologicalSpaceProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`Filter.Eventually.mono` `CompleteSpace.prod` `ImplicitFunctionData.prod_map_implicitFunction`
`contDiffAt` 📖	mathematical	`IsContDiffImplicitAt`	`ContDiffAt` `DenselyNormedField.toNontriviallyNormedField` `RCLike.toDenselyNormedField` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	—
`contDiffAt_implicitFunction` 📖	mathematical	`IsContDiffImplicitAt`	`ContDiffAt` `DenselyNormedField.toNontriviallyNormedField` `RCLike.toDenselyNormedField` `implicitFunction`	—	`CompleteSpace.prod` `ImplicitFunctionData.contDiff_implicitFunction` `contDiffAt_fst` `contDiffAt` `ne_zero` `implicitFunction_def` `ContDiffAt.snd` `ContDiffAt.fun_comp` `ContDiffAt.prodMk` `contDiffAt_fun_id` `contDiffAt_const`
`eventually_implicitFunction_apply_eq` 📖	mathematical	`IsContDiffImplicitAt`	`Filter.Eventually` `nhds` `instTopologicalSpaceProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`Filter.Eventually.mono` `CompleteSpace.prod` `ImplicitFunctionData.implicitFunction_apply_image`
`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` `SeminormedAddCommGroup.toAddCommGroup`	—	—
`implicitFunctionAux_fst` 📖	mathematical	`IsContDiffImplicitAt`	`Filter.Eventually` `implicitFunctionAux` `nhds` `instTopologicalSpaceProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`Filter.Eventually.mono` `CompleteSpace.prod` `ImplicitFunctionData.prod_map_implicitFunction`
`implicitFunctionData_leftFun_apply` 📖	mathematical	`IsContDiffImplicitAt`	`ImplicitFunctionData.leftFun` `DenselyNormedField.toNontriviallyNormedField` `RCLike.toDenselyNormedField` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `CompleteSpace.prod` `PseudoEMetricSpace.toUniformSpace` `PseudoMetricSpace.toPseudoEMetricSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `implicitFunctionData`	—	`CompleteSpace.prod`
`implicitFunctionData_leftFun_pt` 📖	mathematical	`IsContDiffImplicitAt`	`ImplicitFunctionData.leftFun` `DenselyNormedField.toNontriviallyNormedField` `RCLike.toDenselyNormedField` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `CompleteSpace.prod` `PseudoEMetricSpace.toUniformSpace` `PseudoMetricSpace.toPseudoEMetricSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `implicitFunctionData` `ImplicitFunctionData.pt`	—	—
`implicitFunctionData_pt` 📖	mathematical	`IsContDiffImplicitAt`	`ImplicitFunctionData.pt` `DenselyNormedField.toNontriviallyNormedField` `RCLike.toDenselyNormedField` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `CompleteSpace.prod` `PseudoEMetricSpace.toUniformSpace` `PseudoMetricSpace.toPseudoEMetricSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `implicitFunctionData`	—	`CompleteSpace.prod`
`implicitFunctionData_rightFun_apply` 📖	mathematical	`IsContDiffImplicitAt`	`ImplicitFunctionData.rightFun` `DenselyNormedField.toNontriviallyNormedField` `RCLike.toDenselyNormedField` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `CompleteSpace.prod` `PseudoEMetricSpace.toUniformSpace` `PseudoMetricSpace.toPseudoEMetricSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `implicitFunctionData`	—	`CompleteSpace.prod`
`implicitFunctionData_rightFun_pt` 📖	mathematical	`IsContDiffImplicitAt`	`ImplicitFunctionData.rightFun` `DenselyNormedField.toNontriviallyNormedField` `RCLike.toDenselyNormedField` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `CompleteSpace.prod` `PseudoEMetricSpace.toUniformSpace` `PseudoMetricSpace.toPseudoEMetricSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `implicitFunctionData` `ImplicitFunctionData.pt`	—	—
`implicitFunction_apply` 📖	mathematical	`IsContDiffImplicitAt`	`implicitFunction` `ImplicitFunctionData.implicitFunction` `DenselyNormedField.toNontriviallyNormedField` `RCLike.toDenselyNormedField` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `CompleteSpace.prod` `PseudoEMetricSpace.toUniformSpace` `PseudoMetricSpace.toPseudoEMetricSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `implicitFunctionData`	—	—
`implicitFunction_def` 📖	mathematical	`IsContDiffImplicitAt`	`implicitFunction` `ImplicitFunctionData.implicitFunction` `DenselyNormedField.toNontriviallyNormedField` `RCLike.toDenselyNormedField` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `CompleteSpace.prod` `PseudoEMetricSpace.toUniformSpace` `PseudoMetricSpace.toPseudoEMetricSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `implicitFunctionData`	—	—
`ne_zero` 📖	—	`IsContDiffImplicitAt`	—	—	—
`one_le` 📖	mathematical	`IsContDiffImplicitAt`	`WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	`ENat.one_le_iff_ne_zero_withTop` `ne_zero`

(root)

Definitions

Name	Category	Theorems
`IsContDiffImplicitAt` 📖	CompData	—

---

← Back to Index