Documentation Verification Report

DiffContOnCl

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

Statistics

Metric	Count
Definitions `DiffContOnCl`	1
Theorems `add`, `add_const`, `comp`, `const_add`, `const_smul`, `const_sub`, `continuousOn`, `continuousOn_ball`, `differentiableAt`, `differentiableAt'`, `differentiableOn`, `inv`, `mk_ball`, `mono`, `neg`, `smul`, `smul_const`, `sub`, `sub_const`, `comp_diffContOnCl`, `diffContOnCl`, `diffContOnCl`, `diffContOnCl_ball`, `diffContOnCl_iff`, `diffContOnCl_const`, `diffContOnCl_univ`	26
Total	27

DiffContOnCl

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`DiffContOnCl`	`DiffContOnCl` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`DifferentiableOn.add` `differentiableOn` `ContinuousOn.add` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `continuousOn`
`add_const` 📖	mathematical	`DiffContOnCl`	`DiffContOnCl` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`add` `diffContOnCl_const`
`comp` 📖	mathematical	`DiffContOnCl` `Set.MapsTo`	`DiffContOnCl`	—	`DifferentiableOn.comp` `differentiableOn` `ContinuousOn.comp` `continuousOn` `Set.MapsTo.closure_of_continuousOn`
`const_add` 📖	mathematical	`DiffContOnCl`	`DiffContOnCl` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`add` `diffContOnCl_const`
`const_smul` 📖	mathematical	`DiffContOnCl`	`DiffContOnCl` `Function.hasSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid`	—	`DifferentiableOn.const_smul` `differentiableOn` `ContinuousOn.const_smul` `continuousOn`
`const_sub` 📖	mathematical	`DiffContOnCl`	`DiffContOnCl` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`sub` `diffContOnCl_const`
`continuousOn` 📖	mathematical	`DiffContOnCl`	`ContinuousOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `closure`	—	—
`continuousOn_ball` 📖	mathematical	`DiffContOnCl` `Metric.ball` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`ContinuousOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Metric.closedBall`	—	`eq_or_ne` `Metric.closedBall_zero` `continuousOn_singleton` `closure_ball` `continuousOn`
`differentiableAt` 📖	mathematical	`DiffContOnCl` `IsOpen` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set` `Set.instMembership`	`DifferentiableAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`DifferentiableOn.differentiableAt` `differentiableOn` `IsOpen.mem_nhds`
`differentiableAt'` 📖	mathematical	`DiffContOnCl` `Set` `Filter` `Filter.instMembership` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`DifferentiableAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`DifferentiableOn.differentiableAt` `differentiableOn`
`differentiableOn` 📖	mathematical	`DiffContOnCl`	`DifferentiableOn` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	—
`inv` 📖	mathematical	`DiffContOnCl` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	`DiffContOnCl` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace` `Pi.instInv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield` `NormedField.toField`	—	`DifferentiableOn.comp` `differentiableOn_inv` `differentiableOn` `subset_closure` `ContinuousOn.inv₀` `IsTopologicalDivisionRing.toContinuousInv₀` `NormedDivisionRing.to_isTopologicalDivisionRing` `continuousOn`
`mk_ball` 📖	mathematical	`DifferentiableOn` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Metric.ball` `ContinuousOn` `Metric.closedBall`	`DiffContOnCl` `Metric.ball` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`ContinuousOn.mono` `Metric.closure_ball_subset_closedBall`
`mono` 📖	mathematical	`DiffContOnCl` `Set` `Set.instHasSubset`	`DiffContOnCl`	—	`DifferentiableOn.mono` `differentiableOn` `ContinuousOn.mono` `continuousOn` `closure_mono`
`neg` 📖	mathematical	`DiffContOnCl`	`DiffContOnCl` `Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`DifferentiableOn.neg` `differentiableOn` `ContinuousOn.neg` `IsTopologicalAddGroup.toContinuousNeg` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `continuousOn`
`smul` 📖	mathematical	`DiffContOnCl` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedAlgebra.toNormedSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	`DiffContOnCl` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule`	—	`DifferentiableOn.smul` `NormedSpace.toIsBoundedSMul` `differentiableOn` `ContinuousOn.smul` `IsBoundedSMul.continuousSMul` `continuousOn`
`smul_const` 📖	mathematical	`DiffContOnCl` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedAlgebra.toNormedSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	`DiffContOnCl` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule`	—	`smul` `diffContOnCl_const`
`sub` 📖	mathematical	`DiffContOnCl`	`DiffContOnCl` `Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`DifferentiableOn.sub` `differentiableOn` `ContinuousOn.sub` `IsTopologicalAddGroup.to_continuousSub` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `continuousOn`
`sub_const` 📖	mathematical	`DiffContOnCl`	`DiffContOnCl` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`sub` `diffContOnCl_const`

Differentiable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_diffContOnCl` 📖	mathematical	`Differentiable` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DiffContOnCl`	`DiffContOnCl`	—	`DiffContOnCl.comp` `diffContOnCl` `Set.mapsTo_image`
`diffContOnCl` 📖	mathematical	`Differentiable` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	`DiffContOnCl`	—	`differentiableOn` `Continuous.continuousOn` `continuous` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul`

DifferentiableOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`diffContOnCl` 📖	mathematical	`DifferentiableOn` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `closure`	`DiffContOnCl`	—	`mono` `subset_closure` `continuousOn` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul`
`diffContOnCl_ball` 📖	mathematical	`DifferentiableOn` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Set` `Set.instHasSubset` `Metric.closedBall`	`DiffContOnCl` `Metric.ball` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`DiffContOnCl.mk_ball` `mono` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Metric.ball_subset_closedBall` `ContinuousOn.mono` `continuousOn` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul`

IsClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`diffContOnCl_iff` 📖	mathematical	—	`DiffContOnCl` `DifferentiableOn` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`DiffContOnCl.differentiableOn` `DifferentiableOn.continuousOn` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `closure_eq`

(root)

Definitions

Name	Category	Theorems
`DiffContOnCl` 📖	CompData	24 math math: `DiffContOnCl.smul`, `DiffContOnCl.mono`, `DiffContOnCl.add_const`, `DiffContOnCl.sub_const`, `Differentiable.diffContOnCl`, `DiffContOnCl.inv`, `DiffContOnCl.comp`, `DifferentiableOn.diffContOnCl_ball`, `DiffContOnCl.mk_ball`, `DiffContOnCl.const_smul`, `diffContOnCl_const`, `DiffContOnCl.smul_const`, `Complex.HadamardThreeLines.diffContOnCl_interpStrip`, `DiffContOnCl.const_sub`, `DifferentiableOn.diffContOnCl`, `DiffContOnCl.sub`, `DiffContOnCl.add`, `IsClosed.diffContOnCl_iff`, `DiffContOnCl.const_add`, `Complex.HadamardThreeLines.scale_diffContOnCl`, `Complex.HadamardThreeLines.diffContOnCl_invInterpStrip`, `Differentiable.comp_diffContOnCl`, `diffContOnCl_univ`, `DiffContOnCl.neg`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`diffContOnCl_const` 📖	mathematical	—	`DiffContOnCl`	—	`differentiableOn_const` `continuousOn_const`
`diffContOnCl_univ` 📖	mathematical	—	`DiffContOnCl` `Set.univ` `Differentiable` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`IsClosed.diffContOnCl_iff` `isClosed_univ` `differentiableOn_univ`

---

← Back to Index