Basic

📁 Source: Mathlib/Geometry/Manifold/MFDeriv/Basic.lean

Statistics

Metric	Count
Definitions	0
Theorems `mdifferentiable`, `mdifferentiableAt`, `mdifferentiableWithinAt`, `mdifferentiableAt`, `mdifferentiableOn`, `mdifferentiableWithinAt`, `mdifferentiableAt_iff`, `mdifferentiableWithinAt_iff`, `mdifferentiablefWithinAt_iff`, `mfderivWithin_eq`, `mfderivWithin_eq_of_mem`, `mfderiv_eq`, `comp`, `comp_hasMFDerivWithinAt`, `congr_mfderiv`, `congr_of_eventuallyEq`, `continuousAt`, `hasMFDerivWithinAt`, `mdifferentiableAt`, `mfderiv`, `comp`, `congr_mfderiv`, `congr_mono`, `congr_of_eventuallyEq`, `continuousWithinAt`, `hasMFDerivAt`, `insert`, `insert'`, `mdifferentiableWithinAt`, `mfderivWithin`, `mfderivWithin_eq_zero`, `mono`, `mono_of_mem_nhdsWithin`, `of_insert`, `union`, `uniqueMDiffOn`, `uniqueMDiffWithinAt`, `comp`, `comp_mdifferentiableOn`, `continuous`, `mdifferentiableAt`, `mdifferentiableOn`, `mfderivWithin`, `comp`, `comp_mdifferentiableWithinAt`, `comp_mdifferentiableWithinAt_of_eq`, `comp_of_eq`, `congr_of_eventuallyEq`, `hasMFDerivAt`, `mdifferentiableWithinAt`, `mfderiv`, `comp`, `congr_mono`, `continuousOn`, `iUnion_of_isOpen`, `mdifferentiableAt`, `mono`, `union_of_isOpen`, `comp`, `comp_of_eq`, `comp_of_preimage_mem_nhdsWithin`, `comp_of_preimage_mem_nhdsWithin_of_eq`, `congr'`, `congr_mono`, `congr_nhds`, `congr_of_eventuallyEq`, `congr_of_eventuallyEq_insert`, `congr_of_eventuallyEq_of_mem`, `congr_of_mem`, `hasMFDerivWithinAt`, `insert`, `insert'`, `mdifferentiableAt`, `mfderivWithin`, `mfderivWithin_congr_mono`, `mfderivWithin_mono`, `mfderivWithin_mono_of_mem_nhdsWithin`, `mono`, `mono_of_mem_nhdsWithin`, `of_insert`, `eq`, `inter`, `prod`, `eq`, `inter`, `inter'`, `mono`, `mono_nhds`, `mono_of_mem_nhdsWithin`, `prod`, `hasMFDerivAt_unique`, `hasMFDerivWithinAt_congr_set`, `hasMFDerivWithinAt_congr_set'`, `hasMFDerivWithinAt_diff_singleton`, `hasMFDerivWithinAt_insert`, `hasMFDerivWithinAt_inter`, `hasMFDerivWithinAt_inter'`, `hasMFDerivWithinAt_univ`, `mdifferentiableAt_iff_of_mem_source`, `mdifferentiableAt_iff_source_of_mem_source`, `mdifferentiableAt_iff_target`, `mdifferentiableAt_iff_target_of_mem_source`, `mdifferentiableAt_of_isInvertible_mfderiv`, `mdifferentiableOn_congr`, `mdifferentiableOn_empty`, `mdifferentiableOn_iUnion_iff_of_isOpen`, `mdifferentiableOn_iff`, `mdifferentiableOn_iff_of_mem_maximalAtlas`, `mdifferentiableOn_iff_of_mem_maximalAtlas'`, `mdifferentiableOn_iff_of_subset_source`, `mdifferentiableOn_iff_of_subset_source'`, `mdifferentiableOn_iff_target`, `mdifferentiableOn_of_locally_mdifferentiableOn`, `mdifferentiableOn_union_iff_of_isOpen`, `mdifferentiableOn_univ`, `mdifferentiableWithinAt_congr`, `mdifferentiableWithinAt_congr_nhds`, `mdifferentiableWithinAt_congr_of_mem`, `mdifferentiableWithinAt_congr_set`, `mdifferentiableWithinAt_congr_set'`, `mdifferentiableWithinAt_iff`, `mdifferentiableWithinAt_iff_exists_hasMFDerivWithinAt`, `mdifferentiableWithinAt_iff_image`, `mdifferentiableWithinAt_iff_of_mem_maximalAtlas`, `mdifferentiableWithinAt_iff_of_mem_source`, `mdifferentiableWithinAt_iff_of_mem_source'`, `mdifferentiableWithinAt_iff_source_of_mem_maximalAtlas`, `mdifferentiableWithinAt_iff_source_of_mem_source`, `mdifferentiableWithinAt_iff_target`, `mdifferentiableWithinAt_iff_target_inter`, `mdifferentiableWithinAt_iff_target_inter'`, `mdifferentiableWithinAt_iff_target_of_mem_source`, `mdifferentiableWithinAt_insert`, `mdifferentiableWithinAt_insert_self`, `mdifferentiableWithinAt_inter`, `mdifferentiableWithinAt_inter'`, `mdifferentiableWithinAt_of_isInvertible_mfderivWithin`, `mdifferentiableWithinAt_univ`, `mdifferentiable_iff`, `mdifferentiable_iff_target`, `mdifferentiable_of_mdifferentiableOn_iUnion_of_isOpen`, `mdifferentiable_of_mdifferentiableOn_union_of_isOpen`, `mdifferentiable_of_subsingleton`, `mfderivWithin_comp`, `mfderivWithin_comp_of_eq`, `mfderivWithin_comp_of_preimage_mem_nhdsWithin`, `mfderivWithin_comp_of_preimage_mem_nhdsWithin_of_eq`, `mfderivWithin_congr`, `mfderivWithin_congr_of_mem`, `mfderivWithin_congr_set`, `mfderivWithin_congr_set'`, `mfderivWithin_eq_mfderiv`, `mfderivWithin_eventually_congr_set`, `mfderivWithin_eventually_congr_set'`, `mfderivWithin_inter`, `mfderivWithin_of_isOpen`, `mfderivWithin_of_mem_nhds`, `mfderivWithin_subset`, `mfderivWithin_univ`, `mfderivWithin_zero_of_not_mdifferentiableWithinAt`, `mfderiv_comp`, `mfderiv_comp_apply`, `mfderiv_comp_apply_of_eq`, `mfderiv_comp_mfderivWithin`, `mfderiv_comp_mfderivWithin_of_eq`, `mfderiv_comp_of_eq`, `mfderiv_congr`, `mfderiv_congr_point`, `mfderiv_zero_of_not_mdifferentiableAt`, `preimage_extChartAt_eventuallyEq_compl_singleton`, `tangentMapWithin_comp_at`, `tangentMapWithin_congr`, `tangentMapWithin_eq_tangentMap`, `tangentMapWithin_proj`, `tangentMapWithin_snd`, `tangentMapWithin_subset`, `tangentMapWithin_univ`, `tangentMap_comp`, `tangentMap_comp_at`, `tangentMap_proj`, `tangentMap_snd`, `uniqueMDiffOn_univ`, `uniqueMDiffWithinAt_iff`, `uniqueMDiffWithinAt_iff_inter_range`, `uniqueMDiffWithinAt_univ`, `writtenInExtChartAt_comp`	186
Total	186

ContMDiff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mdifferentiable` 📖	mathematical	`ContMDiff`	`MDifferentiable`	—	`ContMDiffAt.mdifferentiableAt`
`mdifferentiableAt` 📖	mathematical	`ContMDiff`	`MDifferentiableAt`	—	`ContMDiffAt.mdifferentiableAt` `contMDiffAt`
`mdifferentiableWithinAt` 📖	mathematical	`ContMDiff`	`MDifferentiableWithinAt`	—	`MDifferentiableAt.mdifferentiableWithinAt` `ContMDiffAt.mdifferentiableAt` `contMDiffAt`

ContMDiffAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mdifferentiableAt` 📖	mathematical	`ContMDiffAt`	`MDifferentiableAt`	—	`mdifferentiableWithinAt_univ` `ContMDiffWithinAt.mdifferentiableWithinAt`

ContMDiffOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mdifferentiableOn` 📖	mathematical	`ContMDiffOn`	`MDifferentiableOn`	—	`ContMDiffWithinAt.mdifferentiableWithinAt`

ContMDiffWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mdifferentiableWithinAt` 📖	mathematical	`ContMDiffWithinAt`	`MDifferentiableWithinAt`	—	`mdifferentiableWithinAt_iff` `ContinuousWithinAt.mono` `ChartedSpace.LiftPropWithinAt.continuousWithinAt` `Set.inter_subset_left` `DifferentiableWithinAt.mono` `ContDiffWithinAt.differentiableWithinAt` `ChartedSpace.LiftPropWithinAt.prop` `ModelWithCorners.source_eq` `Set.inter_univ` `mdifferentiableWithinAt_inter'` `ContinuousWithinAt.preimage_mem_nhdsWithin` `extChartAt_source_mem_nhds`

Filter.EventuallyEq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mdifferentiableAt_iff` 📖	mathematical	`Filter.EventuallyEq` `nhds`	`MDifferentiableAt`	—	`StructureGroupoid.LocalInvariantProp.liftPropAt_congr_iff_of_eventuallyEq` `differentiableWithinAt_localInvariantProp`
`mdifferentiableWithinAt_iff` 📖	mathematical	`Filter.EventuallyEq` `nhdsWithin`	`MDifferentiableWithinAt`	—	`mdifferentiablefWithinAt_iff` `symm`
`mdifferentiablefWithinAt_iff` 📖	mathematical	`Filter.EventuallyEq` `nhdsWithin`	`MDifferentiableWithinAt`	—	`StructureGroupoid.LocalInvariantProp.liftPropWithinAt_congr_iff_of_eventuallyEq` `differentiableWithinAt_localInvariantProp`
`mfderivWithin_eq` 📖	mathematical	`Filter.EventuallyEq` `nhdsWithin`	`mfderivWithin`	—	`mdifferentiableWithinAt_iff` `fderivWithin_eq` `Filter.mp_mem` `extChartAt_preimage_mem_nhdsWithin` `Filter.univ_mem'` `ModelWithCorners.left_inv` `OpenPartialHomeomorph.left_inv`
`mfderivWithin_eq_of_mem` 📖	mathematical	`Filter.EventuallyEq` `nhdsWithin` `Set` `Set.instMembership`	`mfderivWithin`	—	`mfderivWithin_eq` `mem_of_mem_nhdsWithin`
`mfderiv_eq` 📖	mathematical	`Filter.EventuallyEq` `nhds`	`mfderiv`	—	`mem_of_mem_nhds` `mfderivWithin_univ` `mfderivWithin_eq` `nhdsWithin_univ`

HasMFDerivAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	mathematical	`HasMFDerivAt`	`ContinuousLinearMap.comp` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `RingHomCompTriple.ids`	—	`RingHomCompTriple.ids` `hasMFDerivWithinAt_univ` `HasMFDerivWithinAt.comp` `HasMFDerivWithinAt.mono` `Set.subset_univ` `Set.subset_preimage_univ`
`comp_hasMFDerivWithinAt` 📖	mathematical	`HasMFDerivAt` `HasMFDerivWithinAt`	`ContinuousLinearMap.comp` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `RingHomCompTriple.ids`	—	`HasMFDerivWithinAt.comp` `HasMFDerivWithinAt.mono` `hasMFDerivWithinAt_univ` `Set.subset_univ` `Set.subset_preimage_univ`
`congr_mfderiv` 📖	—	`HasMFDerivAt`	—	—	—
`congr_of_eventuallyEq` 📖	—	`HasMFDerivAt` `Filter.EventuallyEq` `nhds`	—	—	`hasMFDerivWithinAt_univ` `HasMFDerivWithinAt.congr_of_eventuallyEq` `nhdsWithin_univ` `mem_of_mem_nhds`
`continuousAt` 📖	mathematical	`HasMFDerivAt`	`ContinuousAt`	—	—
`hasMFDerivWithinAt` 📖	mathematical	`HasMFDerivAt`	`HasMFDerivWithinAt`	—	`ContinuousAt.continuousWithinAt` `HasFDerivWithinAt.mono` `Set.inter_subset_right`
`mdifferentiableAt` 📖	mathematical	`HasMFDerivAt`	`MDifferentiableAt`	—	`mdifferentiableAt_iff`
`mfderiv` 📖	mathematical	`HasMFDerivAt`	`mfderiv`	—	`hasMFDerivAt_unique` `MDifferentiableAt.hasMFDerivAt` `mdifferentiableAt`

HasMFDerivWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	mathematical	`HasMFDerivWithinAt` `Set` `Set.instHasSubset` `Set.preimage`	`ContinuousLinearMap.comp` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `RingHomCompTriple.ids`	—	`RingHomCompTriple.ids` `ContinuousWithinAt.comp` `extChartAt_preimage_mem_nhdsWithin` `ContinuousWithinAt.preimage_mem_nhdsWithin` `extChartAt_source_mem_nhds` `hasFDerivWithinAt_inter'` `extChartAt_preimage_inter_eq` `ModelWithCorners.left_inv` `OpenPartialHomeomorph.left_inv` `HasFDerivWithinAt.comp` `ModelWithCorners.source_eq` `Set.inter_univ` `HasFDerivWithinAt.congr_of_eventuallyEq` `writtenInExtChartAt_comp`
`congr_mfderiv` 📖	—	`HasMFDerivWithinAt`	—	—	—
`congr_mono` 📖	—	`HasMFDerivWithinAt` `Set` `Set.instHasSubset`	—	—	`congr_of_eventuallyEq` `mono` `Filter.mem_inf_of_right`
`congr_of_eventuallyEq` 📖	—	`HasMFDerivWithinAt` `Filter.EventuallyEq` `nhdsWithin`	—	—	`ContinuousWithinAt.congr_of_eventuallyEq` `HasFDerivWithinAt.congr_of_eventuallyEq` `extChartAt_preimage_mem_nhdsWithin` `Filter.mem_of_superset` `ModelWithCorners.left_inv` `OpenPartialHomeomorph.left_inv`
`continuousWithinAt` 📖	mathematical	`HasMFDerivWithinAt`	`ContinuousWithinAt`	—	—
`hasMFDerivAt` 📖	mathematical	`HasMFDerivWithinAt` `Set` `Filter` `Filter.instMembership` `nhds`	`HasMFDerivAt`	—	`hasMFDerivWithinAt_univ` `hasMFDerivWithinAt_inter` `Set.univ_inter`
`insert` 📖	mathematical	`HasMFDerivWithinAt`	`Set` `Set.instInsert`	—	`insert'`
`insert'` 📖	mathematical	`HasMFDerivWithinAt`	`Set` `Set.instInsert`	—	`hasMFDerivWithinAt_insert`
`mdifferentiableWithinAt` 📖	mathematical	`HasMFDerivWithinAt`	`MDifferentiableWithinAt`	—	—
`mfderivWithin` 📖	mathematical	`HasMFDerivWithinAt` `UniqueMDiffWithinAt`	`mfderivWithin`	—	`ContinuousLinearMap.ext` `UniqueMDiffWithinAt.eq` `MDifferentiableWithinAt.hasMFDerivWithinAt` `mdifferentiableWithinAt`
`mfderivWithin_eq_zero` 📖	mathematical	`HasMFDerivWithinAt` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `ContinuousLinearMap.zero`	`mfderivWithin`	—	`mdifferentiableWithinAt` `fderivWithin_def`
`mono` 📖	—	`HasMFDerivWithinAt` `Set` `Set.instHasSubset`	—	—	`ContinuousWithinAt.mono` `HasFDerivWithinAt.mono` `Set.inter_subset_inter` `Set.preimage_mono` `Set.Subset.refl`
`mono_of_mem_nhdsWithin` 📖	—	`HasMFDerivWithinAt` `Set` `Filter` `Filter.instMembership` `nhdsWithin`	—	—	`hasMFDerivWithinAt_inter'` `mono` `Set.inter_subset_right`
`of_insert` 📖	—	`HasMFDerivWithinAt` `Set` `Set.instInsert`	—	—	`hasMFDerivWithinAt_insert`
`union` 📖	mathematical	`HasMFDerivWithinAt`	`Set` `Set.instUnion`	—	`ContinuousWithinAt.union` `Set.union_inter_distrib_right` `HasFDerivWithinAt.union`

IsOpen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`uniqueMDiffOn` 📖	mathematical	`IsOpen`	`UniqueMDiffOn`	—	`uniqueMDiffWithinAt`
`uniqueMDiffWithinAt` 📖	mathematical	`IsOpen` `Set` `Set.instMembership`	`UniqueMDiffWithinAt`	—	`UniqueMDiffWithinAt.mono_of_mem_nhdsWithin` `uniqueMDiffWithinAt_univ` `nhdsWithin_le_nhds` `mem_nhds`

MDifferentiable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	—	`MDifferentiable`	—	—	`MDifferentiableAt.comp`
`comp_mdifferentiableOn` 📖	—	`MDifferentiable` `MDifferentiableOn`	—	—	`MDifferentiableOn.comp` `mdifferentiableOn_univ`
`continuous` 📖	mathematical	`MDifferentiable`	`Continuous`	—	`continuous_iff_continuousAt` `MDifferentiableAt.continuousAt`
`mdifferentiableAt` 📖	mathematical	`MDifferentiable`	`MDifferentiableAt`	—	—
`mdifferentiableOn` 📖	mathematical	`MDifferentiable`	`MDifferentiableOn`	—	`MDifferentiableOn.mono` `mdifferentiableOn_univ` `Set.subset_univ`
`mfderivWithin` 📖	mathematical	`MDifferentiableAt` `UniqueMDiffWithinAt`	`mfderivWithin` `mfderiv`	—	`HasMFDerivWithinAt.mfderivWithin` `HasMFDerivAt.hasMFDerivWithinAt` `MDifferentiableAt.hasMFDerivAt`

MDifferentiableAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	—	`MDifferentiableAt`	—	—	`HasMFDerivAt.mdifferentiableAt` `RingHomCompTriple.ids` `HasMFDerivAt.comp` `hasMFDerivAt`
`comp_mdifferentiableWithinAt` 📖	—	`MDifferentiableAt` `MDifferentiableWithinAt`	—	—	`MDifferentiableWithinAt.comp` `mdifferentiableWithinAt_univ`
`comp_mdifferentiableWithinAt_of_eq` 📖	—	`MDifferentiableAt` `MDifferentiableWithinAt`	—	—	`comp_mdifferentiableWithinAt`
`comp_of_eq` 📖	—	`MDifferentiableAt`	—	—	`comp`
`congr_of_eventuallyEq` 📖	—	`MDifferentiableAt` `Filter.EventuallyEq` `nhds`	—	—	`HasMFDerivAt.mdifferentiableAt` `HasMFDerivAt.congr_of_eventuallyEq` `hasMFDerivAt`
`hasMFDerivAt` 📖	mathematical	`MDifferentiableAt`	`HasMFDerivAt` `mfderiv`	—	`continuousAt` `DifferentiableWithinAt.hasFDerivWithinAt` `differentiableWithinAt_writtenInExtChartAt`
`mdifferentiableWithinAt` 📖	mathematical	`MDifferentiableAt`	`MDifferentiableWithinAt`	—	`MDifferentiableWithinAt.mono` `Set.subset_univ` `mdifferentiableWithinAt_univ`
`mfderiv` 📖	mathematical	`MDifferentiableAt`	`mfderiv` `fderivWithin` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `writtenInExtChartAt` `Set.range` `ModelWithCorners.toFun'` `PartialEquiv.toFun` `extChartAt`	—	—

MDifferentiableOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	—	`MDifferentiableOn` `Set` `Set.instHasSubset` `Set.preimage`	—	—	`MDifferentiableWithinAt.comp`
`congr_mono` 📖	—	`MDifferentiableOn` `Set` `Set.instHasSubset`	—	—	`MDifferentiableWithinAt.congr_mono`
`continuousOn` 📖	mathematical	`MDifferentiableOn`	`ContinuousOn`	—	`MDifferentiableWithinAt.continuousWithinAt`
`iUnion_of_isOpen` 📖	mathematical	`MDifferentiableOn` `IsOpen`	`Set.iUnion`	—	`MDifferentiableAt.mdifferentiableWithinAt` `mdifferentiableAt` `IsOpen.mem_nhds`
`mdifferentiableAt` 📖	mathematical	`MDifferentiableOn` `Set` `Filter` `Filter.instMembership` `nhds`	`MDifferentiableAt`	—	`MDifferentiableWithinAt.mdifferentiableAt` `mem_of_mem_nhds`
`mono` 📖	—	`MDifferentiableOn` `Set` `Set.instHasSubset`	—	—	`MDifferentiableWithinAt.mono`
`union_of_isOpen` 📖	mathematical	`MDifferentiableOn` `IsOpen`	`Set` `Set.instUnion`	—	`MDifferentiableAt.mdifferentiableWithinAt` `MDifferentiableWithinAt.mdifferentiableAt` `IsOpen.mem_nhds`

MDifferentiableWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	—	`MDifferentiableWithinAt` `Set` `Set.instHasSubset` `Set.preimage`	—	—	`ChartedSpace.LiftPropWithinAt.prop` `ChartedSpace.LiftPropWithinAt.continuousWithinAt` `HasMFDerivWithinAt.mdifferentiableWithinAt` `RingHomCompTriple.ids` `HasMFDerivWithinAt.comp`
`comp_of_eq` 📖	—	`MDifferentiableWithinAt` `Set` `Set.instHasSubset` `Set.preimage`	—	—	`comp`
`comp_of_preimage_mem_nhdsWithin` 📖	—	`MDifferentiableWithinAt` `Set` `Filter` `Filter.instMembership` `nhdsWithin` `Set.preimage`	—	—	`mono_of_mem_nhdsWithin` `comp` `mono` `Set.inter_subset_right` `Set.inter_subset_left` `Filter.inter_mem` `self_mem_nhdsWithin`
`comp_of_preimage_mem_nhdsWithin_of_eq` 📖	—	`MDifferentiableWithinAt` `Set` `Filter` `Filter.instMembership` `nhdsWithin` `Set.preimage`	—	—	`comp_of_preimage_mem_nhdsWithin`
`congr'` 📖	—	`MDifferentiableWithinAt` `Set` `Set.instHasSubset` `Set.instMembership`	—	—	`congr`
`congr_mono` 📖	—	`MDifferentiableWithinAt` `Set` `Set.instHasSubset`	—	—	`HasMFDerivWithinAt.mdifferentiableWithinAt` `HasMFDerivWithinAt.congr_mono` `hasMFDerivWithinAt`
`congr_nhds` 📖	—	`MDifferentiableWithinAt` `nhdsWithin`	—	—	`mono_of_mem_nhdsWithin` `self_mem_nhdsWithin`
`congr_of_eventuallyEq` 📖	—	`MDifferentiableWithinAt` `Filter.EventuallyEq` `nhdsWithin`	—	—	`HasMFDerivWithinAt.mdifferentiableWithinAt` `HasMFDerivWithinAt.congr_of_eventuallyEq` `hasMFDerivWithinAt`
`congr_of_eventuallyEq_insert` 📖	—	`MDifferentiableWithinAt` `Filter.EventuallyEq` `nhdsWithin` `Set` `Set.instInsert`	—	—	`of_insert` `congr_of_eventuallyEq_of_mem` `insert` `Set.mem_insert`
`congr_of_eventuallyEq_of_mem` 📖	—	`MDifferentiableWithinAt` `Filter.EventuallyEq` `nhdsWithin` `Set` `Set.instMembership`	—	—	`congr_of_eventuallyEq` `mem_of_mem_nhdsWithin`
`congr_of_mem` 📖	—	`MDifferentiableWithinAt` `Set` `Set.instMembership`	—	—	`StructureGroupoid.LocalInvariantProp.liftPropWithinAt_congr_of_mem` `differentiableWithinAt_localInvariantProp`
`hasMFDerivWithinAt` 📖	mathematical	`MDifferentiableWithinAt`	`HasMFDerivWithinAt` `mfderivWithin`	—	`ChartedSpace.LiftPropWithinAt.continuousWithinAt` `DifferentiableWithinAt.hasFDerivWithinAt` `ChartedSpace.LiftPropWithinAt.prop`
`insert` 📖	mathematical	`MDifferentiableWithinAt`	`Set` `Set.instInsert`	—	`insert'`
`insert'` 📖	mathematical	`MDifferentiableWithinAt`	`Set` `Set.instInsert`	—	`mdifferentiableWithinAt_insert`
`mdifferentiableAt` 📖	mathematical	`MDifferentiableWithinAt` `Set` `Filter` `Filter.instMembership` `nhds`	`MDifferentiableAt`	—	`Set.univ_inter` `mdifferentiableWithinAt_univ` `mdifferentiableWithinAt_inter`
`mfderivWithin` 📖	mathematical	`MDifferentiableWithinAt`	`mfderivWithin` `fderivWithin` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `writtenInExtChartAt` `Set` `Set.instInter` `Set.preimage` `PartialEquiv.toFun` `PartialEquiv.symm` `extChartAt` `Set.range` `ModelWithCorners.toFun'`	—	—
`mfderivWithin_congr_mono` 📖	mathematical	`MDifferentiableWithinAt` `UniqueMDiffWithinAt` `Set` `Set.instHasSubset`	`mfderivWithin`	—	`HasMFDerivWithinAt.mfderivWithin` `HasMFDerivWithinAt.congr_mono` `hasMFDerivWithinAt`
`mfderivWithin_mono` 📖	mathematical	`MDifferentiableWithinAt` `UniqueMDiffWithinAt` `Set` `Set.instHasSubset`	`mfderivWithin`	—	`mfderivWithin_congr_mono`
`mfderivWithin_mono_of_mem_nhdsWithin` 📖	mathematical	`MDifferentiableWithinAt` `UniqueMDiffWithinAt` `Set` `Filter` `Filter.instMembership` `nhdsWithin`	`mfderivWithin`	—	`HasMFDerivWithinAt.mfderivWithin` `HasMFDerivWithinAt.mono_of_mem_nhdsWithin` `hasMFDerivWithinAt`
`mono` 📖	—	`Set` `Set.instHasSubset` `MDifferentiableWithinAt`	—	—	`ContinuousWithinAt.mono` `ChartedSpace.LiftPropWithinAt.continuousWithinAt` `DifferentiableWithinAt.mono` `differentiableWithinAt_writtenInExtChartAt` `Set.inter_subset_inter_left` `Set.preimage_mono`
`mono_of_mem_nhdsWithin` 📖	—	`MDifferentiableWithinAt` `Set` `Filter` `Filter.instMembership` `nhdsWithin`	—	—	`HasMFDerivWithinAt.mdifferentiableWithinAt` `HasMFDerivWithinAt.mono_of_mem_nhdsWithin` `hasMFDerivWithinAt`
`of_insert` 📖	—	`MDifferentiableWithinAt` `Set` `Set.instInsert`	—	—	`mdifferentiableWithinAt_insert`

UniqueMDiffOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq` 📖	—	`UniqueMDiffOn` `Set` `Set.instMembership` `HasMFDerivWithinAt`	—	—	`UniqueMDiffWithinAt.eq`
`inter` 📖	mathematical	`UniqueMDiffOn` `IsOpen`	`Set` `Set.instInter`	—	`UniqueMDiffWithinAt.inter` `IsOpen.mem_nhds`
`prod` 📖	mathematical	`UniqueMDiffOn`	`Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace` `SProd.sprod` `Set` `Set.instSProd`	—	`UniqueMDiffWithinAt.prod`

UniqueMDiffWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq` 📖	—	`UniqueMDiffWithinAt` `HasMFDerivWithinAt`	—	—	`UniqueDiffWithinAt.eq` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace`
`inter` 📖	mathematical	`UniqueMDiffWithinAt` `Set` `Filter` `Filter.instMembership` `nhds`	`Set.instInter`	—	`inter'` `nhdsWithin_le_nhds`
`inter'` 📖	mathematical	`UniqueMDiffWithinAt` `Set` `Filter` `Filter.instMembership` `nhdsWithin`	`Set.instInter`	—	`mono_of_mem_nhdsWithin` `Filter.inter_mem` `self_mem_nhdsWithin`
`mono` 📖	—	`UniqueMDiffWithinAt` `Set` `Set.instHasSubset`	—	—	`UniqueDiffWithinAt.mono` `Set.inter_subset_inter` `Set.preimage_mono` `Set.Subset.refl`
`mono_nhds` 📖	—	`UniqueMDiffWithinAt` `Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `nhdsWithin`	—	—	`UniqueDiffWithinAt.mono_nhds` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Filter.map_mono`
`mono_of_mem_nhdsWithin` 📖	—	`UniqueMDiffWithinAt` `Set` `Filter` `Filter.instMembership` `nhdsWithin`	—	—	`mono_nhds` `nhdsWithin_le_iff`
`prod` 📖	mathematical	`UniqueMDiffWithinAt`	`Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace` `SProd.sprod` `Set` `Set.instSProd`	—	`UniqueDiffWithinAt.mono` `UniqueDiffWithinAt.prod` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `ModelWithCorners.range_prod` `Set.prod_inter_prod` `subset_refl` `Set.instReflSubset`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasMFDerivAt_unique` 📖	—	`HasMFDerivAt`	—	—	`UniqueMDiffWithinAt.eq` `uniqueMDiffWithinAt_univ` `hasMFDerivWithinAt_univ`
`hasMFDerivWithinAt_congr_set` 📖	mathematical	`Filter.EventuallyEq` `nhds`	`HasMFDerivWithinAt`	—	`hasMFDerivWithinAt_congr_set'` `Filter.EventuallyEq.filter_mono` `inf_le_left`
`hasMFDerivWithinAt_congr_set'` 📖	mathematical	`Filter.EventuallyEq` `nhdsWithin` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet`	`HasMFDerivWithinAt`	—	`ModelWithCorners.t1Space` `continuousWithinAt_congr_set'` `hasFDerivWithinAt_congr_set'` `T2Space.t1Space` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `preimage_extChartAt_eventuallyEq_compl_singleton`
`hasMFDerivWithinAt_diff_singleton` 📖	mathematical	—	`HasMFDerivWithinAt` `Set` `Set.instSDiff` `Set.instSingletonSet`	—	`hasMFDerivWithinAt_insert` `Set.insert_diff_singleton`
`hasMFDerivWithinAt_insert` 📖	mathematical	—	`HasMFDerivWithinAt` `Set` `Set.instInsert`	—	`ModelWithCorners.t1Space` `HasMFDerivWithinAt.mono` `Set.subset_insert` `eq_or_ne` `HasMFDerivWithinAt.eq_1` `ContinuousWithinAt.insert` `nhdsWithin_mono` `Set.inter_subset_right` `extChartAt_target_mem_nhdsWithin` `hasFDerivWithinAt_inter'` `HasFDerivWithinAt.mono` `HasFDerivWithinAt.insert` `mem_extChartAt_source` `PartialEquiv.eq_symm_apply` `HasMFDerivWithinAt.mono_of_mem_nhdsWithin` `nhdsWithin_insert_of_ne`
`hasMFDerivWithinAt_inter` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds`	`HasMFDerivWithinAt` `Set.instInter`	—	`HasMFDerivWithinAt.eq_1` `extChartAt_preimage_inter_eq` `hasFDerivWithinAt_inter` `extChartAt_preimage_mem_nhds` `continuousWithinAt_inter`
`hasMFDerivWithinAt_inter'` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhdsWithin`	`HasMFDerivWithinAt` `Set.instInter`	—	`HasMFDerivWithinAt.eq_1` `extChartAt_preimage_inter_eq` `hasFDerivWithinAt_inter'` `extChartAt_preimage_mem_nhdsWithin` `continuousWithinAt_inter'`
`hasMFDerivWithinAt_univ` 📖	mathematical	—	`HasMFDerivWithinAt` `Set.univ` `HasMFDerivAt`	—	`Set.univ_inter`
`mdifferentiableAt_iff_of_mem_source` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv` `chartAt`	`MDifferentiableAt` `ContinuousAt` `DifferentiableWithinAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `PartialEquiv.toFun` `extChartAt` `PartialEquiv.symm` `Set.range` `ModelWithCorners.toFun'`	—	`mdifferentiableWithinAt_iff_of_mem_source` `continuousWithinAt_univ` `Set.preimage_univ` `Set.univ_inter`
`mdifferentiableAt_iff_source_of_mem_source` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv` `chartAt`	`MDifferentiableAt` `MDifferentiableWithinAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `PartialEquiv.toFun` `PartialEquiv.symm` `extChartAt` `Set.range` `ModelWithCorners.toFun'`	—	`mdifferentiableWithinAt_iff_source_of_mem_source` `Set.univ_inter`
`mdifferentiableAt_iff_target` 📖	mathematical	—	`MDifferentiableAt` `ContinuousAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `PartialEquiv.toFun` `extChartAt`	—	`mdifferentiableWithinAt_univ` `mdifferentiableWithinAt_iff_target` `continuousWithinAt_univ`
`mdifferentiableAt_iff_target_of_mem_source` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv` `chartAt`	`MDifferentiableAt` `ContinuousAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `PartialEquiv.toFun` `extChartAt`	—	`mdifferentiableWithinAt_univ` `mdifferentiableWithinAt_iff_target_of_mem_source` `continuousWithinAt_univ`
`mdifferentiableAt_of_isInvertible_mfderiv` 📖	mathematical	`ContinuousLinearMap.IsInvertible` `TangentSpace` `instTopologicalSpaceTangentSpace` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `mfderiv`	`MDifferentiableAt`	—	`mdifferentiableWithinAt_of_isInvertible_mfderivWithin`
`mdifferentiableOn_congr` 📖	mathematical	—	`MDifferentiableOn`	—	`StructureGroupoid.LocalInvariantProp.liftPropOn_congr_iff` `differentiableWithinAt_localInvariantProp`
`mdifferentiableOn_empty` 📖	mathematical	—	`MDifferentiableOn` `Set` `Set.instEmptyCollection`	—	—
`mdifferentiableOn_iUnion_iff_of_isOpen` 📖	mathematical	`IsOpen`	`MDifferentiableOn` `Set.iUnion`	—	`MDifferentiableOn.mono` `Set.subset_iUnion_of_subset` `MDifferentiableOn.iUnion_of_isOpen`
`mdifferentiableOn_iff` 📖	mathematical	—	`MDifferentiableOn` `ContinuousOn` `DifferentiableOn` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `PartialEquiv.toFun` `extChartAt` `PartialEquiv.symm` `Set` `Set.instInter` `PartialEquiv.target` `Set.preimage` `PartialEquiv.source`	—	`ChartedSpace.LiftPropWithinAt.continuousWithinAt` `ModelWithCorners.target_eq` `ModelWithCorners.source_eq` `Set.inter_univ` `OpenPartialHomeomorph.right_inv` `ModelWithCorners.right_inv` `DifferentiableWithinAt.mono` `mdifferentiableWithinAt_iff_of_mem_source` `StructureGroupoid.LocalInvariantProp.liftPropWithinAt_iff` `differentiableWithinAt_localInvariantProp` `Set.ext` `ModelWithCorners.left_inv` `OpenPartialHomeomorph.left_inv`
`mdifferentiableOn_iff_of_mem_maximalAtlas` 📖	mathematical	`OpenPartialHomeomorph` `Set` `Set.instMembership` `IsManifold.maximalAtlas` `WithTop` `ENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `Set.instHasSubset` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv` `Set.MapsTo`	`MDifferentiableOn` `ContinuousOn` `DifferentiableOn` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `PartialEquiv.toFun` `OpenPartialHomeomorph.extend` `PartialEquiv.symm` `Set.image`	—	`mdifferentiableWithinAt_iff_image`
`mdifferentiableOn_iff_of_mem_maximalAtlas'` 📖	mathematical	`OpenPartialHomeomorph` `Set` `Set.instMembership` `IsManifold.maximalAtlas` `WithTop` `ENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `Set.instHasSubset` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv` `Set.MapsTo`	`MDifferentiableOn` `DifferentiableOn` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `PartialEquiv.toFun` `OpenPartialHomeomorph.extend` `PartialEquiv.symm` `Set.image`	—	`mdifferentiableOn_iff_of_mem_maximalAtlas` `OpenPartialHomeomorph.continuousOn_writtenInExtend_iff` `DifferentiableOn.continuousOn` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul`
`mdifferentiableOn_iff_of_subset_source` 📖	mathematical	`Set` `Set.instHasSubset` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv` `chartAt` `Set.MapsTo`	`MDifferentiableOn` `ContinuousOn` `DifferentiableOn` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `PartialEquiv.toFun` `extChartAt` `PartialEquiv.symm` `Set.image`	—	`mdifferentiableOn_iff_of_mem_maximalAtlas` `IsManifold.chart_mem_maximalAtlas`
`mdifferentiableOn_iff_of_subset_source'` 📖	mathematical	`Set` `Set.instHasSubset` `PartialEquiv.source` `extChartAt` `Set.MapsTo`	`MDifferentiableOn` `DifferentiableOn` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `PartialEquiv.toFun` `PartialEquiv.symm` `Set.image`	—	`mdifferentiableOn_iff_of_mem_maximalAtlas'` `IsManifold.chart_mem_maximalAtlas` `extChartAt_source`
`mdifferentiableOn_iff_target` 📖	mathematical	—	`MDifferentiableOn` `ContinuousOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `PartialEquiv.toFun` `extChartAt` `Set` `Set.instInter` `Set.preimage` `PartialEquiv.source`	—	`IsManifold.instOfNatWithTopENat_1` `IsManifold.instOfNatWithTopENat_2` `IsManifold.instOfTopWithTopENat` `Nat.instAtLeastTwoHAddOfNat` `instIsManifoldModelSpace` `PartialEquiv.refl_trans` `ModelWithCorners.source_eq` `Set.inter_univ` `Continuous.continuousOn` `ModelWithCorners.continuous` `ContinuousOn.comp_inter` `OpenPartialHomeomorph.continuousOn_toFun`
`mdifferentiableOn_of_locally_mdifferentiableOn` 📖	—	`IsOpen` `Set` `Set.instMembership` `MDifferentiableOn` `Set.instInter`	—	—	`mdifferentiableWithinAt_inter` `IsOpen.mem_nhds`
`mdifferentiableOn_union_iff_of_isOpen` 📖	mathematical	`IsOpen`	`MDifferentiableOn` `Set` `Set.instUnion`	—	`MDifferentiableOn.mono` `Set.subset_union_left` `Set.subset_union_right` `MDifferentiableOn.union_of_isOpen`
`mdifferentiableOn_univ` 📖	mathematical	—	`MDifferentiableOn` `Set.univ` `MDifferentiable`	—	—
`mdifferentiableWithinAt_congr` 📖	mathematical	—	`MDifferentiableWithinAt`	—	`StructureGroupoid.LocalInvariantProp.liftPropWithinAt_congr_iff` `differentiableWithinAt_localInvariantProp`
`mdifferentiableWithinAt_congr_nhds` 📖	mathematical	`nhdsWithin`	`MDifferentiableWithinAt`	—	`MDifferentiableWithinAt.congr_nhds`
`mdifferentiableWithinAt_congr_of_mem` 📖	mathematical	`Set` `Set.instMembership`	`MDifferentiableWithinAt`	—	`StructureGroupoid.LocalInvariantProp.liftPropWithinAt_congr_iff_of_mem` `differentiableWithinAt_localInvariantProp`
`mdifferentiableWithinAt_congr_set` 📖	mathematical	`Filter.EventuallyEq` `nhds`	`MDifferentiableWithinAt`	—	`hasMFDerivWithinAt_congr_set`
`mdifferentiableWithinAt_congr_set'` 📖	mathematical	`Filter.EventuallyEq` `nhdsWithin` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet`	`MDifferentiableWithinAt`	—	`hasMFDerivWithinAt_congr_set'`
`mdifferentiableWithinAt_iff` 📖	mathematical	—	`MDifferentiableWithinAt` `ContinuousWithinAt` `DifferentiableWithinAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `PartialEquiv.toFun` `extChartAt` `PartialEquiv.symm` `Set` `Set.instInter` `Set.preimage` `Set.range` `ModelWithCorners.toFun'`	—	—
`mdifferentiableWithinAt_iff_exists_hasMFDerivWithinAt` 📖	mathematical	—	`MDifferentiableWithinAt` `HasMFDerivWithinAt`	—	`MDifferentiableWithinAt.hasMFDerivWithinAt` `HasMFDerivWithinAt.mdifferentiableWithinAt`
`mdifferentiableWithinAt_iff_image` 📖	mathematical	`OpenPartialHomeomorph` `Set` `Set.instMembership` `IsManifold.maximalAtlas` `WithTop` `ENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `Set.instHasSubset` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv`	`MDifferentiableWithinAt` `ContinuousWithinAt` `DifferentiableWithinAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `PartialEquiv.toFun` `OpenPartialHomeomorph.extend` `PartialEquiv.symm` `Set.image`	—	`mdifferentiableWithinAt_iff_of_mem_maximalAtlas` `differentiableWithinAt_congr_nhds` `OpenPartialHomeomorph.extend_symm_preimage_inter_range_eventuallyEq`
`mdifferentiableWithinAt_iff_of_mem_maximalAtlas` 📖	mathematical	`OpenPartialHomeomorph` `Set` `Set.instMembership` `IsManifold.maximalAtlas` `WithTop` `ENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv`	`MDifferentiableWithinAt` `ContinuousWithinAt` `DifferentiableWithinAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `PartialEquiv.toFun` `OpenPartialHomeomorph.extend` `PartialEquiv.symm` `Set.instInter` `Set.preimage` `Set.range` `ModelWithCorners.toFun'`	—	`StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart` `differentiableWithinAt_localInvariantProp` `IsManifold.toHasGroupoid`
`mdifferentiableWithinAt_iff_of_mem_source` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv` `chartAt`	`MDifferentiableWithinAt` `ContinuousWithinAt` `DifferentiableWithinAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `PartialEquiv.toFun` `extChartAt` `PartialEquiv.symm` `Set.instInter` `Set.preimage` `Set.range` `ModelWithCorners.toFun'`	—	`mdifferentiableWithinAt_iff_of_mem_maximalAtlas` `IsManifold.chart_mem_maximalAtlas`
`mdifferentiableWithinAt_iff_of_mem_source'` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv` `chartAt`	`MDifferentiableWithinAt` `ContinuousWithinAt` `DifferentiableWithinAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `PartialEquiv.toFun` `extChartAt` `PartialEquiv.symm` `Set.instInter` `PartialEquiv.target` `Set.preimage`	—	`mdifferentiableWithinAt_iff_of_mem_source` `differentiableWithinAt_congr_nhds` `PartialEquiv.image_source_inter_eq'` `map_extChartAt_nhdsWithin_eq_image'` `extChartAt_source` `map_extChartAt_nhdsWithin'` `Set.inter_comm` `nhdsWithin_inter_of_mem` `extChartAt_source_mem_nhds'`
`mdifferentiableWithinAt_iff_source_of_mem_maximalAtlas` 📖	mathematical	`OpenPartialHomeomorph` `Set` `Set.instMembership` `IsManifold.maximalAtlas` `WithTop` `ENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv`	`MDifferentiableWithinAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `PartialEquiv.toFun` `PartialEquiv.symm` `OpenPartialHomeomorph.extend` `Set.instInter` `Set.preimage` `Set.range` `ModelWithCorners.toFun'`	—	`StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart_source` `differentiableWithinAt_localInvariantProp` `IsManifold.toHasGroupoid` `OpenPartialHomeomorph.extend_symm_continuousWithinAt_comp_right_iff` `OpenPartialHomeomorph.left_inv` `PartialEquiv.left_inv` `OpenPartialHomeomorph.extend_source`
`mdifferentiableWithinAt_iff_source_of_mem_source` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv` `chartAt`	`MDifferentiableWithinAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `PartialEquiv.toFun` `PartialEquiv.symm` `extChartAt` `Set.instInter` `Set.preimage` `Set.range` `ModelWithCorners.toFun'`	—	`mdifferentiableWithinAt_iff_source_of_mem_maximalAtlas` `IsManifold.chart_mem_maximalAtlas`
`mdifferentiableWithinAt_iff_target` 📖	mathematical	—	`MDifferentiableWithinAt` `ContinuousWithinAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `PartialEquiv.toFun` `extChartAt`	—	`ContinuousAt.comp_continuousWithinAt` `continuousAt_extChartAt`
`mdifferentiableWithinAt_iff_target_inter` 📖	mathematical	—	`MDifferentiableWithinAt` `ContinuousWithinAt` `DifferentiableWithinAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `writtenInExtChartAt` `Set` `Set.instInter` `PartialEquiv.target` `extChartAt` `Set.preimage` `PartialEquiv.toFun` `PartialEquiv.symm`	—	`mdifferentiableWithinAt_iff'` `Set.inter_comm` `nhdsWithin_inter` `nhdsWithin_extChartAt_target_eq`
`mdifferentiableWithinAt_iff_target_inter'` 📖	mathematical	—	`MDifferentiableWithinAt` `ContinuousWithinAt` `DifferentiableWithinAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `PartialEquiv.toFun` `extChartAt` `PartialEquiv.symm` `Set` `Set.instInter` `PartialEquiv.target` `Set.preimage` `PartialEquiv.source`	—	`differentiableWithinAt_congr_nhds` `ContinuousWithinAt.nhdsWithin_extChartAt_symm_preimage_inter_range`
`mdifferentiableWithinAt_iff_target_of_mem_source` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv` `chartAt`	`MDifferentiableWithinAt` `ContinuousWithinAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `PartialEquiv.toFun` `extChartAt`	—	`StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart_target` `differentiableWithinAt_localInvariantProp` `IsManifold.toHasGroupoid` `IsManifold.chart_mem_maximalAtlas` `ContinuousAt.comp_continuousWithinAt` `OpenPartialHomeomorph.continuousAt` `continuousAt_extChartAt'` `extChartAt_source`
`mdifferentiableWithinAt_insert` 📖	mathematical	—	`MDifferentiableWithinAt` `Set` `Set.instInsert`	—	`eq_or_ne` `mdifferentiableWithinAt_insert_self` `ModelWithCorners.t1Space` `mdifferentiableWithinAt_congr_nhds` `nhdsWithin_insert_of_ne`
`mdifferentiableWithinAt_insert_self` 📖	mathematical	—	`MDifferentiableWithinAt` `Set` `Set.instInsert`	—	`MDifferentiableWithinAt.mono` `Set.subset_insert` `HasMFDerivWithinAt.mdifferentiableWithinAt` `HasMFDerivWithinAt.insert` `MDifferentiableWithinAt.hasMFDerivWithinAt`
`mdifferentiableWithinAt_inter` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds`	`MDifferentiableWithinAt` `Set.instInter`	—	`MDifferentiableWithinAt.eq_1` `StructureGroupoid.LocalInvariantProp.liftPropWithinAt_inter` `differentiableWithinAt_localInvariantProp`
`mdifferentiableWithinAt_inter'` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhdsWithin`	`MDifferentiableWithinAt` `Set.instInter`	—	`MDifferentiableWithinAt.eq_1` `StructureGroupoid.LocalInvariantProp.liftPropWithinAt_inter'` `differentiableWithinAt_localInvariantProp`
`mdifferentiableWithinAt_of_isInvertible_mfderivWithin` 📖	mathematical	`ContinuousLinearMap.IsInvertible` `TangentSpace` `instTopologicalSpaceTangentSpace` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `mfderivWithin`	`MDifferentiableWithinAt`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `mfderivWithin_zero_of_not_mdifferentiableWithinAt` `Mathlib.Tactic.Contrapose.contrapose₄` `ContinuousLinearMap.isInvertible_zero_iff` `MDifferentiableAt.mdifferentiableWithinAt` `MDifferentiable.mdifferentiableAt` `mdifferentiable_of_subsingleton`
`mdifferentiableWithinAt_univ` 📖	mathematical	—	`MDifferentiableWithinAt` `Set.univ` `MDifferentiableAt`	—	—
`mdifferentiable_iff` 📖	mathematical	—	`MDifferentiable` `Continuous` `DifferentiableOn` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `PartialEquiv.toFun` `extChartAt` `PartialEquiv.symm` `Set` `Set.instInter` `PartialEquiv.target` `Set.preimage` `PartialEquiv.source`	—	`ModelWithCorners.target_eq` `ModelWithCorners.source_eq` `Set.inter_univ` `Set.univ_inter`
`mdifferentiable_iff_target` 📖	mathematical	—	`MDifferentiable` `Continuous` `MDifferentiableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `PartialEquiv.toFun` `extChartAt` `Set.preimage` `PartialEquiv.source`	—	`mdifferentiableOn_univ` `mdifferentiableOn_iff_target` `ModelWithCorners.source_eq` `Set.inter_univ` `Set.univ_inter`
`mdifferentiable_of_mdifferentiableOn_iUnion_of_isOpen` 📖	mathematical	`MDifferentiableOn` `IsOpen` `Set.iUnion` `Set.univ`	`MDifferentiable`	—	`mdifferentiableOn_univ` `MDifferentiableOn.iUnion_of_isOpen`
`mdifferentiable_of_mdifferentiableOn_union_of_isOpen` 📖	mathematical	`MDifferentiableOn` `Set` `Set.instUnion` `Set.univ` `IsOpen`	`MDifferentiable`	—	`mdifferentiableOn_univ` `MDifferentiableOn.union_of_isOpen`
`mdifferentiable_of_subsingleton` 📖	mathematical	—	`MDifferentiable`	—	`Function.Injective.subsingleton` `ModelWithCorners.injective` `ChartedSpace.discreteTopology` `Subsingleton.discreteTopology` `Continuous.continuousAt` `continuous_of_discreteTopology` `DifferentiableAt.differentiableWithinAt` `HasFDerivAt.differentiableAt` `hasFDerivAt_of_subsingleton`
`mfderivWithin_comp` 📖	mathematical	`MDifferentiableWithinAt` `Set` `Set.instHasSubset` `Set.preimage` `UniqueMDiffWithinAt`	`mfderivWithin` `ContinuousLinearMap.comp` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `RingHomCompTriple.ids`	—	`HasMFDerivWithinAt.mfderivWithin` `RingHomCompTriple.ids` `HasMFDerivWithinAt.comp` `MDifferentiableWithinAt.hasMFDerivWithinAt`
`mfderivWithin_comp_of_eq` 📖	mathematical	`MDifferentiableWithinAt` `Set` `Set.instHasSubset` `Set.preimage` `UniqueMDiffWithinAt`	`mfderivWithin` `ContinuousLinearMap.comp` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `RingHomCompTriple.ids`	—	`RingHomCompTriple.ids` `mfderivWithin_comp`
`mfderivWithin_comp_of_preimage_mem_nhdsWithin` 📖	mathematical	`MDifferentiableWithinAt` `Set` `Filter` `Filter.instMembership` `nhdsWithin` `Set.preimage` `UniqueMDiffWithinAt`	`mfderivWithin` `ContinuousLinearMap.comp` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `RingHomCompTriple.ids`	—	`Filter.inter_mem` `self_mem_nhdsWithin` `MDifferentiableWithinAt.mfderivWithin_mono_of_mem_nhdsWithin` `MDifferentiableWithinAt.comp` `MDifferentiableWithinAt.mono` `Set.inter_subset_left` `Set.inter_subset_right` `RingHomCompTriple.ids` `mfderivWithin_comp` `UniqueMDiffWithinAt.inter'`
`mfderivWithin_comp_of_preimage_mem_nhdsWithin_of_eq` 📖	mathematical	`MDifferentiableWithinAt` `Set` `Filter` `Filter.instMembership` `nhdsWithin` `Set.preimage` `UniqueMDiffWithinAt`	`mfderivWithin` `ContinuousLinearMap.comp` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `RingHomCompTriple.ids`	—	`RingHomCompTriple.ids` `mfderivWithin_comp_of_preimage_mem_nhdsWithin`
`mfderivWithin_congr` 📖	mathematical	—	`mfderivWithin`	—	`Filter.EventuallyEq.mfderivWithin_eq` `Filter.eventuallyEq_of_mem` `self_mem_nhdsWithin`
`mfderivWithin_congr_of_mem` 📖	mathematical	`Set` `Set.instMembership`	`mfderivWithin`	—	`Filter.EventuallyEq.mfderivWithin_eq_of_mem` `Filter.eventuallyEq_of_mem` `self_mem_nhdsWithin`
`mfderivWithin_congr_set` 📖	mathematical	`Filter.EventuallyEq` `nhds`	`mfderivWithin`	—	`mfderivWithin_congr_set'` `Filter.EventuallyEq.filter_mono` `inf_le_left`
`mfderivWithin_congr_set'` 📖	mathematical	`Filter.EventuallyEq` `nhdsWithin` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet`	`mfderivWithin`	—	`mdifferentiableWithinAt_congr_set'` `fderivWithin_congr_set'` `T2Space.t1Space` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `preimage_extChartAt_eventuallyEq_compl_singleton`
`mfderivWithin_eq_mfderiv` 📖	mathematical	`UniqueMDiffWithinAt` `MDifferentiableAt`	`mfderivWithin` `mfderiv`	—	`mfderivWithin_univ` `mfderivWithin_subset` `Set.subset_univ` `MDifferentiableAt.mdifferentiableWithinAt`
`mfderivWithin_eventually_congr_set` 📖	mathematical	`Filter.EventuallyEq` `nhds`	`Filter.Eventually` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `mfderivWithin`	—	`mfderivWithin_eventually_congr_set'` `Filter.EventuallyEq.filter_mono` `inf_le_left`
`mfderivWithin_eventually_congr_set'` 📖	mathematical	`Filter.EventuallyEq` `nhdsWithin` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet`	`Filter.Eventually` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `mfderivWithin` `nhds`	—	`Filter.Eventually.mono` `eventually_nhds_nhdsWithin` `mfderivWithin_congr_set'`
`mfderivWithin_inter` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds`	`mfderivWithin` `Set.instInter`	—	`mfderivWithin.eq_1` `extChartAt_preimage_inter_eq` `mdifferentiableWithinAt_inter` `fderivWithin_inter` `extChartAt_preimage_mem_nhds`
`mfderivWithin_of_isOpen` 📖	mathematical	`IsOpen` `Set` `Set.instMembership`	`mfderivWithin` `mfderiv`	—	`mfderivWithin_of_mem_nhds` `IsOpen.mem_nhds`
`mfderivWithin_of_mem_nhds` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds`	`mfderivWithin` `mfderiv`	—	`mfderivWithin_univ` `Set.univ_inter` `mfderivWithin_inter`
`mfderivWithin_subset` 📖	mathematical	`Set` `Set.instHasSubset` `UniqueMDiffWithinAt` `MDifferentiableWithinAt`	`mfderivWithin`	—	`HasMFDerivWithinAt.mfderivWithin` `HasMFDerivWithinAt.mono` `MDifferentiableWithinAt.hasMFDerivWithinAt`
`mfderivWithin_univ` 📖	mathematical	—	`mfderivWithin` `Set.univ` `mfderiv`	—	`Set.univ_inter` `mdifferentiableWithinAt_univ`
`mfderivWithin_zero_of_not_mdifferentiableWithinAt` 📖	mathematical	`MDifferentiableWithinAt`	`mfderivWithin` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `ContinuousLinearMap.zero`	—	—
`mfderiv_comp` 📖	mathematical	`MDifferentiableAt`	`mfderiv` `ContinuousLinearMap.comp` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `RingHomCompTriple.ids`	—	`HasMFDerivAt.mfderiv` `RingHomCompTriple.ids` `HasMFDerivAt.comp` `MDifferentiableAt.hasMFDerivAt`
`mfderiv_comp_apply` 📖	mathematical	`MDifferentiableAt`	`DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `ContinuousLinearMap.funLike` `mfderiv`	—	`RingHomCompTriple.ids` `mfderiv_comp`
`mfderiv_comp_apply_of_eq` 📖	mathematical	`MDifferentiableAt`	`DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `ContinuousLinearMap.funLike` `mfderiv`	—	`mfderiv_comp_apply`
`mfderiv_comp_mfderivWithin` 📖	mathematical	`MDifferentiableAt` `MDifferentiableWithinAt` `UniqueMDiffWithinAt`	`mfderivWithin` `ContinuousLinearMap.comp` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `RingHomCompTriple.ids` `mfderiv`	—	`RingHomCompTriple.ids` `mfderivWithin_univ` `mfderivWithin_comp` `MDifferentiableAt.mdifferentiableWithinAt`
`mfderiv_comp_mfderivWithin_of_eq` 📖	mathematical	`MDifferentiableAt` `MDifferentiableWithinAt` `UniqueMDiffWithinAt`	`mfderivWithin` `ContinuousLinearMap.comp` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `RingHomCompTriple.ids` `mfderiv`	—	`RingHomCompTriple.ids` `mfderiv_comp_mfderivWithin`
`mfderiv_comp_of_eq` 📖	mathematical	`MDifferentiableAt`	`mfderiv` `ContinuousLinearMap.comp` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `RingHomCompTriple.ids`	—	`RingHomCompTriple.ids` `mfderiv_comp`
`mfderiv_congr` 📖	mathematical	—	`mfderiv`	—	—
`mfderiv_congr_point` 📖	mathematical	—	`mfderiv`	—	—
`mfderiv_zero_of_not_mdifferentiableAt` 📖	mathematical	`MDifferentiableAt`	`mfderiv` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `ContinuousLinearMap.zero`	—	—
`preimage_extChartAt_eventuallyEq_compl_singleton` 📖	mathematical	`Filter.EventuallyEq` `nhdsWithin` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet`	`UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PartialEquiv.toFun` `extChartAt` `Set.instInter` `Set.preimage` `PartialEquiv.symm` `Set.range` `ModelWithCorners.toFun'`	—	`ModelWithCorners.t1Space` `mem_nhdsWithin_iff_exists_mem_nhds_inter` `nhdsWithin_compl_singleton_le` `nhdsWithin_univ` `Set.union_compl_self` `nhdsWithin_union` `Filter.union_mem_sup` `extChartAt_target_mem_nhdsWithin` `self_mem_nhdsWithin` `Filter.inter_mem` `ContinuousAt.preimage_mem_nhds` `continuousAt_extChartAt_symm` `extChartAt_to_inv` `PartialEquiv.eq_symm_apply` `ModelWithCorners.source_eq` `Set.inter_univ`
`tangentMapWithin_comp_at` 📖	mathematical	`MDifferentiableWithinAt` `Bundle.TotalSpace.proj` `TangentSpace` `Set` `Set.instHasSubset` `Set.preimage` `UniqueMDiffWithinAt`	`tangentMapWithin`	—	`RingHomCompTriple.ids` `mfderivWithin_comp`
`tangentMapWithin_congr` 📖	mathematical	`Set` `Set.instMembership` `Bundle.TotalSpace.proj` `TangentSpace`	`tangentMapWithin`	—	`Bundle.TotalSpace.ext` `tangentMapWithin.eq_1` `mfderivWithin_congr`
`tangentMapWithin_eq_tangentMap` 📖	mathematical	`UniqueMDiffWithinAt` `Bundle.TotalSpace.proj` `TangentSpace` `MDifferentiableAt`	`tangentMapWithin` `tangentMap`	—	`tangentMapWithin_univ` `tangentMapWithin_subset` `Set.subset_univ` `mdifferentiableWithinAt_univ`
`tangentMapWithin_proj` 📖	mathematical	—	`Bundle.TotalSpace.proj` `TangentSpace` `tangentMapWithin`	—	—
`tangentMapWithin_snd` 📖	mathematical	—	`Bundle.TotalSpace.snd` `TangentSpace` `tangentMapWithin` `DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `ContinuousLinearMap.funLike` `mfderivWithin`	—	—
`tangentMapWithin_subset` 📖	mathematical	`Set` `Set.instHasSubset` `UniqueMDiffWithinAt` `Bundle.TotalSpace.proj` `TangentSpace` `MDifferentiableWithinAt`	`tangentMapWithin`	—	`mfderivWithin_subset`
`tangentMapWithin_univ` 📖	mathematical	—	`tangentMapWithin` `Set.univ` `tangentMap`	—	`mfderivWithin_univ`
`tangentMap_comp` 📖	mathematical	`MDifferentiable`	`tangentMap` `TangentBundle`	—	`tangentMap_comp_at`
`tangentMap_comp_at` 📖	mathematical	`MDifferentiableAt` `Bundle.TotalSpace.proj` `TangentSpace`	`tangentMap`	—	`RingHomCompTriple.ids` `mfderiv_comp`
`tangentMap_proj` 📖	mathematical	—	`Bundle.TotalSpace.proj` `TangentSpace` `tangentMap`	—	—
`tangentMap_snd` 📖	mathematical	—	`Bundle.TotalSpace.snd` `TangentSpace` `tangentMap` `DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `ContinuousLinearMap.funLike` `mfderiv`	—	—
`uniqueMDiffOn_univ` 📖	mathematical	—	`UniqueMDiffOn` `Set.univ`	—	`IsOpen.uniqueMDiffOn` `isOpen_univ`
`uniqueMDiffWithinAt_iff` 📖	mathematical	—	`UniqueMDiffWithinAt` `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.instInter` `Set.preimage` `PartialEquiv.toFun` `PartialEquiv.symm` `extChartAt` `PartialEquiv.target`	—	`uniqueDiffWithinAt_congr` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `nhdsWithin_inter` `nhdsWithin_extChartAt_target_eq`
`uniqueMDiffWithinAt_iff_inter_range` 📖	mathematical	—	`UniqueMDiffWithinAt` `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.instInter` `Set.preimage` `PartialEquiv.toFun` `PartialEquiv.symm` `extChartAt` `Set.range` `ModelWithCorners.toFun'`	—	—
`uniqueMDiffWithinAt_univ` 📖	mathematical	—	`UniqueMDiffWithinAt` `Set.univ`	—	`Set.univ_inter` `ModelWithCorners.uniqueDiffOn` `Set.mem_range_self`
`writtenInExtChartAt_comp` 📖	mathematical	`ContinuousWithinAt`	`Filter.EventuallyEq` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PartialEquiv.toFun` `extChartAt` `Set` `Set.instInter` `Set.preimage` `PartialEquiv.symm` `Set.range` `ModelWithCorners.toFun'` `writtenInExtChartAt`	—	`Filter.mem_of_superset` `extChartAt_preimage_mem_nhdsWithin` `ContinuousWithinAt.preimage_mem_nhdsWithin` `extChartAt_source_mem_nhds` `ModelWithCorners.left_inv` `OpenPartialHomeomorph.left_inv` `ModelWithCorners.source_eq` `Set.inter_univ`

---

← Back to Index