Equiv

📁 Source: Mathlib/Analysis/Calculus/FDeriv/Equiv.lean

Statistics

Metric	Count
Definitions	0
Theorems `comp_differentiableAt_iff`, `comp_differentiableOn_iff`, `comp_differentiableWithinAt_iff`, `comp_differentiable_iff`, `comp_fderiv`, `comp_fderivWithin`, `comp_hasFDerivAt_iff`, `comp_hasFDerivAt_iff'`, `comp_hasFDerivWithinAt_iff`, `comp_hasFDerivWithinAt_iff'`, `comp_hasStrictFDerivAt_iff`, `comp_right_differentiableAt_iff`, `comp_right_differentiableOn_iff`, `comp_right_differentiableWithinAt_iff`, `comp_right_differentiable_iff`, `comp_right_fderiv`, `comp_right_fderivWithin`, `comp_right_hasFDerivAt_iff`, `comp_right_hasFDerivAt_iff'`, `comp_right_hasFDerivWithinAt_iff`, `comp_right_hasFDerivWithinAt_iff'`, `differentiable`, `differentiableAt`, `differentiableOn`, `differentiableWithinAt`, `fderiv`, `fderivWithin`, `hasFDerivAt`, `hasFDerivWithinAt`, `hasStrictFDerivAt`, `uniqueDiffOn_image`, `uniqueDiffOn_image_iff`, `uniqueDiffOn_preimage_iff`, `eventually_ne`, `eventually_notMem`, `lim_real`, `of_local_left_inverse`, `tendsto_nhdsNE`, `eventually_ne`, `eventually_notMem`, `mapsTo_tangent_cone`, `of_local_left_inverse`, `tendsto_nhdsWithin_nhdsNE`, `uniqueDiffWithinAt`, `uniqueDiffWithinAt_of_continuousLinearEquiv`, `of_local_left_inverse`, `comp_differentiableAt_iff`, `comp_differentiableOn_iff`, `comp_differentiableWithinAt_iff`, `comp_differentiable_iff`, `comp_fderiv`, `comp_fderiv'`, `comp_fderivWithin`, `comp_hasFDerivAt_iff`, `comp_hasFDerivAt_iff'`, `comp_hasFDerivWithinAt_iff`, `comp_hasFDerivWithinAt_iff'`, `comp_hasStrictFDerivAt_iff`, `differentiable`, `differentiableAt`, `differentiableOn`, `differentiableWithinAt`, `fderiv`, `fderivWithin`, `hasFDerivAt`, `hasFDerivWithinAt`, `hasStrictFDerivAt`, `hasFDerivAt_symm`, `hasStrictFDerivAt_symm`, `image`, `smul`, `smul_iff`, `fderivWithin_comp_smul`, `fderivWithin_comp_smul_eq_fderivWithin_smul`, `fderivWithin_continuousLinearEquiv_comp`, `fderiv_comp_smul`, `fderiv_continuousLinearEquiv_comp`, `fderiv_continuousLinearEquiv_comp'`, `hasFDerivWithinAt_comp_smul_iff_smul`, `hasFDerivWithinAt_comp_smul_smul_iff`, `has_fderiv_at_filter_real_equiv`	81
Total	81

ContinuousLinearEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_differentiableAt_iff` 📖	mathematical	—	`DifferentiableAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `EquivLike.toFunLike` `equivLike`	—	`RingHomInvPair.ids` `differentiableWithinAt_univ` `comp_differentiableWithinAt_iff`
`comp_differentiableOn_iff` 📖	mathematical	—	`DifferentiableOn` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `EquivLike.toFunLike` `equivLike`	—	`RingHomInvPair.ids` `DifferentiableOn.eq_1` `comp_differentiableWithinAt_iff`
`comp_differentiableWithinAt_iff` 📖	mathematical	—	`DifferentiableWithinAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `EquivLike.toFunLike` `equivLike`	—	`RingHomInvPair.ids` `DifferentiableAt.comp_differentiableWithinAt` `Differentiable.differentiableAt` `differentiable` `symm_comp_self` `Function.comp_assoc`
`comp_differentiable_iff` 📖	mathematical	—	`Differentiable` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `EquivLike.toFunLike` `equivLike`	—	`RingHomInvPair.ids` `differentiableOn_univ` `comp_differentiableOn_iff`
`comp_fderiv` 📖	mathematical	—	`fderiv` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `EquivLike.toFunLike` `equivLike` `ContinuousLinearMap.comp` `AddCommGroup.toAddCommMonoid` `RingHomCompTriple.ids` `toContinuousLinearMap` `SeminormedAddCommGroup.toAddCommGroup`	—	`RingHomInvPair.ids` `RingHomCompTriple.ids` `fderivWithin_univ` `comp_fderivWithin` `uniqueDiffWithinAt_univ` `NormedField.nhdsNE_neBot` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul`
`comp_fderivWithin` 📖	mathematical	`UniqueDiffWithinAt` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	`fderivWithin` `DFunLike.coe` `ContinuousLinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `EquivLike.toFunLike` `equivLike` `ContinuousLinearMap.comp` `AddCommGroup.toAddCommMonoid` `RingHomCompTriple.ids` `toContinuousLinearMap` `SeminormedAddCommGroup.toAddCommGroup`	—	`RingHomInvPair.ids` `RingHomCompTriple.ids` `fderiv_comp_fderivWithin` `differentiableAt` `fderiv` `comp_differentiableWithinAt_iff` `fderivWithin_zero_of_not_differentiableWithinAt` `ContinuousLinearMap.comp_zero`
`comp_hasFDerivAt_iff` 📖	mathematical	—	`HasFDerivAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `EquivLike.toFunLike` `equivLike` `ContinuousLinearMap.comp` `AddCommGroup.toAddCommMonoid` `RingHomCompTriple.ids` `toContinuousLinearMap`	—	`RingHomInvPair.ids` `RingHomCompTriple.ids` `comp_hasFDerivWithinAt_iff`
`comp_hasFDerivAt_iff'` 📖	mathematical	—	`HasFDerivAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `EquivLike.toFunLike` `equivLike` `ContinuousLinearMap.comp` `AddCommGroup.toAddCommMonoid` `RingHomCompTriple.ids` `toContinuousLinearMap` `symm`	—	`RingHomInvPair.ids` `RingHomCompTriple.ids` `comp_hasFDerivWithinAt_iff'`
`comp_hasFDerivWithinAt_iff` 📖	mathematical	—	`HasFDerivWithinAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `EquivLike.toFunLike` `equivLike` `ContinuousLinearMap.comp` `AddCommGroup.toAddCommMonoid` `RingHomCompTriple.ids` `toContinuousLinearMap`	—	`RingHomInvPair.ids` `RingHomCompTriple.ids` `symm_apply_apply` `ContinuousLinearMap.comp.congr_simp` `coe_symm_comp_coe` `ContinuousLinearMap.id_comp` `HasFDerivAt.comp_hasFDerivWithinAt` `hasFDerivAt`
`comp_hasFDerivWithinAt_iff'` 📖	mathematical	—	`HasFDerivWithinAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `EquivLike.toFunLike` `equivLike` `ContinuousLinearMap.comp` `AddCommGroup.toAddCommMonoid` `RingHomCompTriple.ids` `toContinuousLinearMap` `symm`	—	`RingHomInvPair.ids` `RingHomCompTriple.ids` `comp_hasFDerivWithinAt_iff` `ContinuousLinearMap.comp_assoc` `RingHomInvPair.triples₂` `coe_comp_coe_symm` `RingHomCompTriple.right_ids` `ContinuousLinearMap.id_comp`
`comp_hasStrictFDerivAt_iff` 📖	mathematical	—	`HasStrictFDerivAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `EquivLike.toFunLike` `equivLike` `ContinuousLinearMap.comp` `AddCommGroup.toAddCommMonoid` `RingHomCompTriple.ids` `toContinuousLinearMap`	—	`RingHomInvPair.ids` `RingHomCompTriple.ids` `symm_apply_apply` `ContinuousLinearMap.ext` `HasStrictFDerivAt.comp` `hasStrictFDerivAt`
`comp_right_differentiableAt_iff` 📖	mathematical	—	`DifferentiableAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `EquivLike.toFunLike` `equivLike`	—	`RingHomInvPair.ids` `comp_right_differentiableWithinAt_iff`
`comp_right_differentiableOn_iff` 📖	mathematical	—	`DifferentiableOn` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `EquivLike.toFunLike` `equivLike` `Set.preimage`	—	`RingHomInvPair.ids` `apply_symm_apply` `comp_right_differentiableWithinAt_iff`
`comp_right_differentiableWithinAt_iff` 📖	mathematical	—	`DifferentiableWithinAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `EquivLike.toFunLike` `equivLike` `Set.preimage`	—	`RingHomInvPair.ids` `DifferentiableWithinAt.comp` `symm_apply_apply` `differentiableWithinAt` `apply_symm_apply` `self_comp_symm` `Function.comp_assoc` `Set.mapsTo_preimage`
`comp_right_differentiable_iff` 📖	mathematical	—	`Differentiable` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `EquivLike.toFunLike` `equivLike`	—	`RingHomInvPair.ids` `comp_right_differentiableOn_iff`
`comp_right_fderiv` 📖	mathematical	—	`fderiv` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `EquivLike.toFunLike` `equivLike` `ContinuousLinearMap.comp` `AddCommGroup.toAddCommMonoid` `RingHomCompTriple.ids` `toContinuousLinearMap`	—	`RingHomInvPair.ids` `RingHomCompTriple.ids` `fderivWithin_univ` `comp_right_fderivWithin` `uniqueDiffWithinAt_univ` `NormedField.nhdsNE_neBot` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `Set.preimage_univ`
`comp_right_fderivWithin` 📖	mathematical	`UniqueDiffWithinAt` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Set.preimage` `DFunLike.coe` `ContinuousLinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `EquivLike.toFunLike` `equivLike`	`fderivWithin` `ContinuousLinearMap.comp` `AddCommGroup.toAddCommMonoid` `RingHomCompTriple.ids` `toContinuousLinearMap`	—	`RingHomInvPair.ids` `RingHomCompTriple.ids` `HasFDerivWithinAt.fderivWithin` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `comp_right_hasFDerivWithinAt_iff` `DifferentiableWithinAt.hasFDerivWithinAt` `comp_right_differentiableWithinAt_iff` `fderivWithin_zero_of_not_differentiableWithinAt` `ContinuousLinearMap.zero_comp`
`comp_right_hasFDerivAt_iff` 📖	mathematical	—	`HasFDerivAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `EquivLike.toFunLike` `equivLike` `ContinuousLinearMap.comp` `AddCommGroup.toAddCommMonoid` `RingHomCompTriple.ids` `toContinuousLinearMap`	—	`RingHomInvPair.ids` `RingHomCompTriple.ids`
`comp_right_hasFDerivAt_iff'` 📖	mathematical	—	`HasFDerivAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `EquivLike.toFunLike` `equivLike` `ContinuousLinearMap.comp` `AddCommGroup.toAddCommMonoid` `RingHomCompTriple.ids` `toContinuousLinearMap` `symm`	—	`RingHomInvPair.ids` `RingHomCompTriple.ids` `comp_right_hasFDerivWithinAt_iff'`
`comp_right_hasFDerivWithinAt_iff` 📖	mathematical	—	`HasFDerivWithinAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `EquivLike.toFunLike` `equivLike` `ContinuousLinearMap.comp` `AddCommGroup.toAddCommMonoid` `RingHomCompTriple.ids` `toContinuousLinearMap` `Set.preimage`	—	`RingHomInvPair.ids` `RingHomCompTriple.ids` `Function.comp_assoc` `self_comp_symm` `ContinuousLinearMap.comp_assoc` `RingHomInvPair.triples₂` `coe_comp_coe_symm` `ContinuousLinearMap.comp_id` `HasFDerivWithinAt.comp` `symm_apply_apply` `hasFDerivWithinAt` `apply_symm_apply` `Set.mapsTo_preimage`
`comp_right_hasFDerivWithinAt_iff'` 📖	mathematical	—	`HasFDerivWithinAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `EquivLike.toFunLike` `equivLike` `Set.preimage` `ContinuousLinearMap.comp` `AddCommGroup.toAddCommMonoid` `RingHomCompTriple.ids` `toContinuousLinearMap` `symm`	—	`RingHomInvPair.ids` `RingHomCompTriple.ids` `comp_right_hasFDerivWithinAt_iff` `ContinuousLinearMap.comp_assoc` `RingHomInvPair.triples₂` `coe_symm_comp_coe` `ContinuousLinearMap.comp_id`
`differentiable` 📖	mathematical	—	`Differentiable` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `EquivLike.toFunLike` `equivLike`	—	`RingHomInvPair.ids` `differentiableAt`
`differentiableAt` 📖	mathematical	—	`DifferentiableAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `EquivLike.toFunLike` `equivLike`	—	`RingHomInvPair.ids` `HasFDerivAt.differentiableAt` `hasFDerivAt`
`differentiableOn` 📖	mathematical	—	`DifferentiableOn` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `EquivLike.toFunLike` `equivLike`	—	`RingHomInvPair.ids` `Differentiable.differentiableOn` `differentiable`
`differentiableWithinAt` 📖	mathematical	—	`DifferentiableWithinAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `EquivLike.toFunLike` `equivLike`	—	`RingHomInvPair.ids` `DifferentiableAt.differentiableWithinAt` `differentiableAt`
`fderiv` 📖	mathematical	—	`fderiv` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `EquivLike.toFunLike` `equivLike` `toContinuousLinearMap`	—	`RingHomInvPair.ids` `HasFDerivAt.fderiv` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `hasFDerivAt`
`fderivWithin` 📖	mathematical	`UniqueDiffWithinAt` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	`fderivWithin` `DFunLike.coe` `ContinuousLinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `EquivLike.toFunLike` `equivLike` `toContinuousLinearMap`	—	`RingHomInvPair.ids` `ContinuousLinearMap.fderivWithin` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace`
`hasFDerivAt` 📖	mathematical	—	`HasFDerivAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `EquivLike.toFunLike` `equivLike` `toContinuousLinearMap`	—	`RingHomInvPair.ids` `ContinuousLinearMap.hasFDerivAtFilter`
`hasFDerivWithinAt` 📖	mathematical	—	`HasFDerivWithinAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `EquivLike.toFunLike` `equivLike` `toContinuousLinearMap`	—	`RingHomInvPair.ids` `ContinuousLinearMap.hasFDerivWithinAt`
`hasStrictFDerivAt` 📖	mathematical	—	`HasStrictFDerivAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `EquivLike.toFunLike` `equivLike` `toContinuousLinearMap`	—	`RingHomInvPair.ids` `ContinuousLinearMap.hasStrictFDerivAt`
`uniqueDiffOn_image` 📖	mathematical	`UniqueDiffOn` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	`Set.image` `DFunLike.coe` `ContinuousLinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `EquivLike.toFunLike` `equivLike`	—	`RingHomInvPair.ids` `UniqueDiffOn.image` `hasFDerivWithinAt` `Function.Surjective.denseRange` `surjective`
`uniqueDiffOn_image_iff` 📖	mathematical	—	`UniqueDiffOn` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Set.image` `DFunLike.coe` `ContinuousLinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `EquivLike.toFunLike` `equivLike`	—	`RingHomInvPair.ids` `uniqueDiffOn_image` `symm_image_image`
`uniqueDiffOn_preimage_iff` 📖	mathematical	—	`UniqueDiffOn` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Set.preimage` `DFunLike.coe` `ContinuousLinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `EquivLike.toFunLike` `equivLike`	—	`RingHomInvPair.ids` `image_symm_eq_preimage` `uniqueDiffOn_image_iff`

HasFDerivAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eventually_ne` 📖	mathematical	`HasFDerivAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `AntilipschitzWith` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.funLike`	`Filter.Eventually` `nhdsWithin` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet`	—	`Set.compl_eq_univ_diff` `HasFDerivWithinAt.eventually_ne` `hasFDerivWithinAt_univ`
`eventually_notMem` 📖	mathematical	`HasFDerivAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `AntilipschitzWith` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.funLike` `AccPt` `Filter.principal`	`Filter.Eventually` `Set` `Set.instMembership` `nhdsWithin` `Compl.compl` `Set.instCompl` `Set.instSingletonSet`	—	`Set.compl_eq_univ_diff` `HasFDerivWithinAt.eventually_notMem` `hasFDerivWithinAt_univ`
`lim_real` 📖	mathematical	`HasFDerivAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `Real.normedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	`Filter.Tendsto` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `Real.instInv` `Filter.atTop` `Real.instPreorder` `nhds` `DFunLike.coe` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `ContinuousLinearMap.funLike`	—	`lim` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `Filter.tendsto_atTop_atTop` `instIsDirectedOrder` `Real.instIsOrderedRing` `Real.instArchimedean` `le_trans` `le_abs_self`
`of_local_left_inverse` 📖	mathematical	`ContinuousAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `HasFDerivAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `ContinuousLinearEquiv.toContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Filter.Eventually` `nhds`	`ContinuousLinearEquiv.symm`	—	`RingHomInvPair.ids` `HasFDerivWithinAt.of_local_left_inverse` `Filter.Tendsto.inf` `Filter.principal_univ` `Set.mem_univ`
`tendsto_nhdsNE` 📖	mathematical	`HasFDerivAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `AntilipschitzWith` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.funLike`	`Filter.Tendsto` `nhdsWithin` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet`	—	`Set.compl_eq_univ_diff` `HasFDerivWithinAt.tendsto_nhdsWithin_nhdsNE` `hasFDerivWithinAt_univ`

HasFDerivWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eventually_ne` 📖	mathematical	`HasFDerivWithinAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `AntilipschitzWith` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.funLike`	`Filter.Eventually` `nhdsWithin` `Set` `Set.instSDiff` `Set.instSingletonSet`	—	`Filter.eventually_map` `Filter.Eventually.filter_mono` `tendsto_nhdsWithin_nhdsNE` `eq_or_ne` `eventually_mem_nhdsWithin` `eventually_ne_nhdsWithin` `T2Space.t1Space` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace`
`eventually_notMem` 📖	mathematical	`HasFDerivWithinAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `AntilipschitzWith` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.funLike` `AccPt` `Filter.principal`	`Filter.Eventually` `Set` `Set.instMembership` `nhdsWithin` `Set.instSDiff` `Set.instSingletonSet`	—	`Filter.eventually_map` `Filter.Eventually.filter_mono` `tendsto_nhdsWithin_nhdsNE` `Filter.not_frequently` `accPt_iff_frequently_nhdsNE`
`mapsTo_tangent_cone` 📖	mathematical	`HasFDerivWithinAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	`Set.MapsTo` `DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.funLike` `tangentConeAt` `NormedAddCommGroup.toAddCommGroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Set.image`	—	`exists_fun_of_mem_tangentConeAt` `mem_tangentConeAt_of_seq` `tendsto_sub_nhds_zero_iff` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Filter.Tendsto.comp` `ContinuousWithinAt.tendsto` `continuousWithinAt` `IsTopologicalAddGroup.toContinuousAdd` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `tendsto_nhdsWithin_iff` `add_zero` `Filter.Tendsto.add` `tendsto_const_nhds` `Filter.Eventually.mono` `add_sub_cancel` `lim`
`of_local_left_inverse` 📖	mathematical	`Filter.Tendsto` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `HasFDerivWithinAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `ContinuousLinearEquiv.toContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Set` `Set.instMembership` `Filter.Eventually`	`ContinuousLinearEquiv.symm`	—	`RingHomInvPair.ids` `Asymptotics.IsBigO.congr` `ContinuousLinearMap.isBigO_comp` `RingHomIsometric.ids` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousSemilinearEquivClass.continuousSemilinearMapClass` `ContinuousLinearEquiv.continuousSemilinearEquivClass` `ContinuousLinearEquiv.symm_apply_apply` `HasFDerivAtFilter.of_isLittleO` `Asymptotics.IsBigO.trans_isLittleO` `Asymptotics.IsLittleO.trans_isBigO` `Asymptotics.IsLittleO.congr'` `Asymptotics.IsLittleO.symm` `Asymptotics.IsLittleO.comp_tendsto` `HasFDerivAtFilter.isLittleO` `Filter.Eventually.mono` `Filter.Eventually.self_of_nhdsWithin` `Filter.EventuallyEq.rfl` `Asymptotics.IsBigO.congr'` `Asymptotics.IsBigO.comp_tendsto` `Asymptotics.IsTheta.isBigO_symm` `HasFDerivAtFilter.isTheta_sub` `Homeomorph.isInducing`
`tendsto_nhdsWithin_nhdsNE` 📖	mathematical	`HasFDerivWithinAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `AntilipschitzWith` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.funLike`	`Filter.Tendsto` `nhdsWithin` `Set` `Set.instSDiff` `Set.instSingletonSet` `Compl.compl` `Set.instCompl`	—	`dist_zero` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass` `AntilipschitzWith.le_mul_dist` `Asymptotics.isBigO_iff` `Filter.Eventually.of_forall` `Asymptotics.IsLittleO.trans_isBigO` `HasFDerivAtFilter.isLittleO` `Asymptotics.IsBigO.eq_zero_imp` `Asymptotics.IsBigO.trans` `Asymptotics.IsEquivalent.isBigO_symm` `le_inf` `LE.le.trans` `Filter.map_mono` `nhdsWithin_mono` `Set.diff_subset` `continuousWithinAt` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `Filter.le_principal_iff` `Filter.eventually_mem_set` `Filter.eventually_map` `Set.diff_eq` `nhdsWithin_inter'` `Filter.eventually_inf_principal`
`uniqueDiffWithinAt` 📖	mathematical	`HasFDerivWithinAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `UniqueDiffWithinAt` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NormedAddCommGroup.toAddCommGroup` `DenseRange` `DFunLike.coe` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.funLike`	`Set.image`	—	`DenseRange.dense_of_mapsTo` `ContinuousLinearMap.continuous` `UniqueDiffWithinAt.dense_tangentConeAt` `Submodule.span_le` `Set.MapsTo.mono` `mapsTo_tangent_cone` `Set.Subset.rfl` `Submodule.subset_span` `ContinuousWithinAt.mem_closure_image` `continuousWithinAt` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `UniqueDiffWithinAt.mem_closure`
`uniqueDiffWithinAt_of_continuousLinearEquiv` 📖	mathematical	`HasFDerivWithinAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ContinuousLinearEquiv.toContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `UniqueDiffWithinAt` `NormedAddCommGroup.toAddCommGroup`	`Set.image`	—	`RingHomInvPair.ids` `uniqueDiffWithinAt` `Function.Surjective.denseRange` `ContinuousLinearEquiv.surjective`

HasStrictFDerivAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_local_left_inverse` 📖	mathematical	`ContinuousAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `HasStrictFDerivAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `ContinuousLinearEquiv.toContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Filter.Eventually` `nhds`	`ContinuousLinearEquiv.symm`	—	`RingHomInvPair.ids` `ContinuousAt.prodMap'` `Filter.Eventually.prodMk_nhds` `Asymptotics.IsBigO.congr` `ContinuousLinearMap.isBigO_comp` `RingHomIsometric.ids` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousSemilinearEquivClass.continuousSemilinearMapClass` `ContinuousLinearEquiv.continuousSemilinearEquivClass` `ContinuousLinearEquiv.symm_apply_apply` `of_isLittleO` `Asymptotics.IsBigO.trans_isLittleO` `Asymptotics.IsLittleO.trans_isBigO` `Asymptotics.IsLittleO.congr'` `Asymptotics.IsLittleO.symm` `Asymptotics.IsLittleO.comp_tendsto` `isLittleO` `Filter.Eventually.mono` `Filter.Eventually.of_forall` `Asymptotics.IsBigO.congr'` `Asymptotics.IsBigO.comp_tendsto` `Asymptotics.IsTheta.isBigO_symm` `isTheta_sub` `Homeomorph.isInducing` `Filter.EventuallyEq.rfl`

LinearIsometryEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_differentiableAt_iff` 📖	mathematical	—	`DifferentiableAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EquivLike.toFunLike` `instEquivLike`	—	`RingHomInvPair.ids` `ContinuousLinearEquiv.comp_differentiableAt_iff`
`comp_differentiableOn_iff` 📖	mathematical	—	`DifferentiableOn` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EquivLike.toFunLike` `instEquivLike`	—	`RingHomInvPair.ids` `ContinuousLinearEquiv.comp_differentiableOn_iff`
`comp_differentiableWithinAt_iff` 📖	mathematical	—	`DifferentiableWithinAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EquivLike.toFunLike` `instEquivLike`	—	`RingHomInvPair.ids` `ContinuousLinearEquiv.comp_differentiableWithinAt_iff`
`comp_differentiable_iff` 📖	mathematical	—	`Differentiable` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EquivLike.toFunLike` `instEquivLike`	—	`RingHomInvPair.ids` `ContinuousLinearEquiv.comp_differentiable_iff`
`comp_fderiv` 📖	mathematical	—	`fderiv` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EquivLike.toFunLike` `instEquivLike` `ContinuousLinearMap.comp` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `RingHomCompTriple.ids` `ContinuousLinearEquiv.toContinuousLinearMap` `toContinuousLinearEquiv`	—	`RingHomInvPair.ids` `ContinuousLinearEquiv.comp_fderiv`
`comp_fderiv'` 📖	mathematical	—	`fderiv` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EquivLike.toFunLike` `instEquivLike` `ContinuousLinearMap.comp` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `RingHomCompTriple.ids` `ContinuousLinearEquiv.toContinuousLinearMap` `toContinuousLinearEquiv`	—	`RingHomInvPair.ids` `RingHomCompTriple.ids` `comp_fderiv`
`comp_fderivWithin` 📖	mathematical	`UniqueDiffWithinAt` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	`fderivWithin` `DFunLike.coe` `LinearIsometryEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EquivLike.toFunLike` `instEquivLike` `ContinuousLinearMap.comp` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `RingHomCompTriple.ids` `ContinuousLinearEquiv.toContinuousLinearMap` `toContinuousLinearEquiv`	—	`RingHomInvPair.ids` `ContinuousLinearEquiv.comp_fderivWithin`
`comp_hasFDerivAt_iff` 📖	mathematical	—	`HasFDerivAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EquivLike.toFunLike` `instEquivLike` `ContinuousLinearMap.comp` `AddCommGroup.toAddCommMonoid` `RingHomCompTriple.ids` `ContinuousLinearEquiv.toContinuousLinearMap` `toContinuousLinearEquiv`	—	`RingHomInvPair.ids` `ContinuousLinearEquiv.comp_hasFDerivAt_iff`
`comp_hasFDerivAt_iff'` 📖	mathematical	—	`HasFDerivAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EquivLike.toFunLike` `instEquivLike` `ContinuousLinearMap.comp` `AddCommGroup.toAddCommMonoid` `RingHomCompTriple.ids` `ContinuousLinearEquiv.toContinuousLinearMap` `toContinuousLinearEquiv` `symm`	—	`RingHomInvPair.ids` `ContinuousLinearEquiv.comp_hasFDerivAt_iff'`
`comp_hasFDerivWithinAt_iff` 📖	mathematical	—	`HasFDerivWithinAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EquivLike.toFunLike` `instEquivLike` `ContinuousLinearMap.comp` `AddCommGroup.toAddCommMonoid` `RingHomCompTriple.ids` `ContinuousLinearEquiv.toContinuousLinearMap` `toContinuousLinearEquiv`	—	`RingHomInvPair.ids` `ContinuousLinearEquiv.comp_hasFDerivWithinAt_iff`
`comp_hasFDerivWithinAt_iff'` 📖	mathematical	—	`HasFDerivWithinAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EquivLike.toFunLike` `instEquivLike` `ContinuousLinearMap.comp` `AddCommGroup.toAddCommMonoid` `RingHomCompTriple.ids` `ContinuousLinearEquiv.toContinuousLinearMap` `toContinuousLinearEquiv` `symm`	—	`RingHomInvPair.ids` `ContinuousLinearEquiv.comp_hasFDerivWithinAt_iff'`
`comp_hasStrictFDerivAt_iff` 📖	mathematical	—	`HasStrictFDerivAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EquivLike.toFunLike` `instEquivLike` `ContinuousLinearMap.comp` `AddCommGroup.toAddCommMonoid` `RingHomCompTriple.ids` `ContinuousLinearEquiv.toContinuousLinearMap` `toContinuousLinearEquiv`	—	`RingHomInvPair.ids` `ContinuousLinearEquiv.comp_hasStrictFDerivAt_iff`
`differentiable` 📖	mathematical	—	`Differentiable` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EquivLike.toFunLike` `instEquivLike`	—	`RingHomInvPair.ids` `differentiableAt`
`differentiableAt` 📖	mathematical	—	`DifferentiableAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EquivLike.toFunLike` `instEquivLike`	—	`RingHomInvPair.ids` `HasFDerivAt.differentiableAt` `hasFDerivAt`
`differentiableOn` 📖	mathematical	—	`DifferentiableOn` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EquivLike.toFunLike` `instEquivLike`	—	`RingHomInvPair.ids` `Differentiable.differentiableOn` `differentiable`
`differentiableWithinAt` 📖	mathematical	—	`DifferentiableWithinAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EquivLike.toFunLike` `instEquivLike`	—	`RingHomInvPair.ids` `DifferentiableAt.differentiableWithinAt` `differentiableAt`
`fderiv` 📖	mathematical	—	`fderiv` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EquivLike.toFunLike` `instEquivLike` `ContinuousLinearEquiv.toContinuousLinearMap` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `toContinuousLinearEquiv`	—	`RingHomInvPair.ids` `HasFDerivAt.fderiv` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `hasFDerivAt`
`fderivWithin` 📖	mathematical	`UniqueDiffWithinAt` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	`fderivWithin` `DFunLike.coe` `LinearIsometryEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EquivLike.toFunLike` `instEquivLike` `ContinuousLinearEquiv.toContinuousLinearMap` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `toContinuousLinearEquiv`	—	`RingHomInvPair.ids` `ContinuousLinearEquiv.fderivWithin`
`hasFDerivAt` 📖	mathematical	—	`HasFDerivAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EquivLike.toFunLike` `instEquivLike` `ContinuousLinearEquiv.toContinuousLinearMap` `AddCommGroup.toAddCommMonoid` `toContinuousLinearEquiv`	—	`RingHomInvPair.ids` `ContinuousLinearEquiv.hasFDerivAt`
`hasFDerivWithinAt` 📖	mathematical	—	`HasFDerivWithinAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EquivLike.toFunLike` `instEquivLike` `ContinuousLinearEquiv.toContinuousLinearMap` `AddCommGroup.toAddCommMonoid` `toContinuousLinearEquiv`	—	`RingHomInvPair.ids` `ContinuousLinearEquiv.hasFDerivWithinAt`
`hasStrictFDerivAt` 📖	mathematical	—	`HasStrictFDerivAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EquivLike.toFunLike` `instEquivLike` `ContinuousLinearEquiv.toContinuousLinearMap` `AddCommGroup.toAddCommMonoid` `toContinuousLinearEquiv`	—	`RingHomInvPair.ids` `ContinuousLinearEquiv.hasStrictFDerivAt`

OpenPartialHomeomorph

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasFDerivAt_symm` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.target` `toPartialEquiv` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `HasFDerivAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `toFun'` `ContinuousLinearEquiv.toContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `symm`	`ContinuousLinearEquiv.symm`	—	`RingHomInvPair.ids` `HasFDerivAt.of_local_left_inverse` `continuousAt` `eventually_right_inverse`
`hasStrictFDerivAt_symm` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.target` `toPartialEquiv` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `HasStrictFDerivAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `toFun'` `ContinuousLinearEquiv.toContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `symm`	`ContinuousLinearEquiv.symm`	—	`RingHomInvPair.ids` `HasStrictFDerivAt.of_local_left_inverse` `continuousAt` `eventually_right_inverse`

UniqueDiffOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`image` 📖	mathematical	`UniqueDiffOn` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `HasFDerivWithinAt` `SeminormedAddCommGroup.toAddCommGroup` `DenseRange` `DFunLike.coe` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.funLike`	`Set.image`	—	`Set.forall_mem_image` `HasFDerivWithinAt.uniqueDiffWithinAt`

UniqueDiffWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`smul` 📖	mathematical	`UniqueDiffWithinAt` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	`Set` `Set.smulSet` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero`	—	`HasFDerivWithinAt.uniqueDiffWithinAt_of_continuousLinearEquiv` `RingHomInvPair.ids` `Units.continuousConstSMul` `Units.smulCommClass_left` `ContinuousLinearEquiv.hasFDerivWithinAt`
`smul_iff` 📖	mathematical	—	`UniqueDiffWithinAt` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Set` `Set.smulSet` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero`	—	`inv_smul_smul₀` `smul` `inv_ne_zero`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fderivWithin_comp_smul` 📖	mathematical	`UniqueDiffWithinAt` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	`fderivWithin` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.instSMul` `AddCommMonoid.toAddMonoid` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `Ring.toSemiring` `CommRing.toRing` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedSpace.toIsBoundedSMul` `Set` `Set.smulSet`	—	`smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `eq_or_ne` `zero_smul` `fderivWithin_fun_const` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `fderivWithin_comp_smul_eq_fderivWithin_smul` `fderivWithin_const_smul_field` `UniqueDiffWithinAt.smul`
`fderivWithin_comp_smul_eq_fderivWithin_smul` 📖	mathematical	—	`fderivWithin` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `Function.hasSMul` `Set` `Set.smulSet`	—	`eq_or_ne` `zero_smul` `fderivWithin_fun_const` `fderivWithin_zero` `hasFDerivWithinAt_comp_smul_iff_smul` `fderivWithin_def`
`fderivWithin_continuousLinearEquiv_comp` 📖	mathematical	`UniqueDiffWithinAt` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	`fderivWithin` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.addCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedSpace.toIsBoundedSMul` `ContinuousLinearMap.topologicalSpace` `ContinuousLinearMap.comp` `RingHomCompTriple.ids` `ContinuousLinearEquiv.toContinuousLinearMap` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `AddCommGroup.toAddGroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `ContinuousLinearEquiv.arrowCongr` `ContinuousLinearEquiv.refl`	—	`RingHomInvPair.ids` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `RingHomCompTriple.ids` `IsTopologicalAddGroup.toContinuousAdd` `RingHomIsometric.ids` `ContinuousLinearEquiv.comp_fderivWithin`
`fderiv_comp_smul` 📖	mathematical	—	`fderiv` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.instSMul` `AddCommMonoid.toAddMonoid` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `Ring.toSemiring` `CommRing.toRing` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedSpace.toIsBoundedSMul`	—	`smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `fderivWithin_univ` `fderivWithin_comp_smul` `uniqueDiffWithinAt_univ` `NormedField.nhdsNE_neBot` `IsBoundedSMul.continuousSMul` `eq_or_ne` `Set.zero_smul_set` `AddTorsor.nonempty` `zero_smul` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Set.smul_set_univ₀`
`fderiv_continuousLinearEquiv_comp` 📖	mathematical	—	`fderiv` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.addCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedSpace.toIsBoundedSMul` `ContinuousLinearMap.topologicalSpace` `ContinuousLinearMap.comp` `RingHomCompTriple.ids` `ContinuousLinearEquiv.toContinuousLinearMap` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `AddCommGroup.toAddGroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `ContinuousLinearEquiv.arrowCongr` `ContinuousLinearEquiv.refl`	—	`RingHomInvPair.ids` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `RingHomCompTriple.ids` `IsTopologicalAddGroup.toContinuousAdd` `RingHomIsometric.ids` `ContinuousLinearEquiv.comp_fderiv`
`fderiv_continuousLinearEquiv_comp'` 📖	mathematical	—	`fderiv` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.addCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedSpace.toIsBoundedSMul` `ContinuousLinearMap.topologicalSpace` `ContinuousLinearMap.comp` `RingHomCompTriple.ids` `ContinuousLinearEquiv.toContinuousLinearMap` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `AddCommGroup.toAddGroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `ContinuousLinearEquiv.arrowCongr` `ContinuousLinearEquiv.refl`	—	`RingHomInvPair.ids` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `RingHomCompTriple.ids` `IsTopologicalAddGroup.toContinuousAdd` `fderiv_continuousLinearEquiv_comp`
`hasFDerivWithinAt_comp_smul_iff_smul` 📖	mathematical	—	`HasFDerivWithinAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `Function.hasSMul` `Set` `Set.smulSet`	—	`smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `CanLift.prf` `instCanLiftUnitsValIsUnit` `RingHomInvPair.ids` `Units.continuousConstSMul` `Units.smulCommClass_left` `RingHomCompTriple.ids` `ContinuousLinearEquiv.comp_hasFDerivWithinAt_iff`
`hasFDerivWithinAt_comp_smul_smul_iff` 📖	mathematical	—	`HasFDerivWithinAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `ContinuousLinearMap.instSMul` `AddCommMonoid.toAddMonoid` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `Ring.toSemiring` `CommRing.toRing` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toIsBoundedSMul` `Set` `Set.smulSet`	—	`smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `eq_or_ne` `zero_smul` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `HasFDerivWithinAt.of_subsingleton` `Set.subsingleton_zero_smul_set` `T2Space.t1Space` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `CanLift.prf` `instCanLiftUnitsValIsUnit` `RingHomCompTriple.ids` `RingHomInvPair.ids` `Units.continuousConstSMul` `Units.smulCommClass_left` `ContinuousLinearMap.ext` `ContinuousLinearMap.map_smul_of_tower` `LinearMap.CompatibleSMul.units` `LinearMap.IsScalarTower.compatibleSMul` `IsScalarTower.left` `Units.smul_def` `ContinuousLinearEquiv.smulLeft_apply_apply` `ContinuousLinearEquiv.comp_right_hasFDerivWithinAt_iff` `Set.preimage_preimage` `inv_smul_smul`
`has_fderiv_at_filter_real_equiv` 📖	mathematical	—	`Filter.Tendsto` `Real` `Real.instMul` `Real.instInv` `Norm.norm` `NormedAddCommGroup.toNorm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `DFunLike.coe` `ContinuousLinearMap` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `ContinuousLinearMap.funLike` `nhds` `Real.pseudoMetricSpace` `Real.instZero` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`tendsto_iff_norm_sub_tendsto_zero` `Filter.tendsto_congr` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass` `sub_zero` `norm_smul` `NormedSpace.toNormSMulClass` `norm_inv` `norm_norm`

---

← Back to Index