ExtChartAt

📁 Source: Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean

Statistics

Metric	Count
Definitions `extend`, `extChartAt`, `writtenInExtChartAt`	3
Theorems `extChartAt_symm_preimage_inter_range_eventuallyEq`, `nhdsWithin_extChartAt_symm_preimage_inter_range`, `of_locallyCompact_manifold`, `of_locallyCompact_manifold`, `locallyCompact_of_finiteDimensional`, `contDiffOn_extend_coord_change`, `contDiffWithinAt_extend_coord_change`, `contDiffWithinAt_extend_coord_change'`, `continuousAt_extend`, `continuousAt_extend_symm`, `continuousAt_extend_symm'`, `continuousOn_extend`, `continuousOn_extend_symm`, `continuousOn_writtenInExtend_iff`, `continuousWithinAt_writtenInExtend_iff`, `extend_coe`, `extend_coe_symm`, `extend_coord_change_source`, `extend_coord_change_source_mem_nhdsWithin`, `extend_coord_change_source_mem_nhdsWithin'`, `extend_image_nhds_mem_nhds_of_boundaryless`, `extend_image_nhds_mem_nhds_of_mem_interior_range`, `extend_image_source_inter`, `extend_image_target_mem_nhds`, `extend_left_inv`, `extend_left_inv'`, `extend_preimage_inter_eq`, `extend_preimage_mem_nhds`, `extend_preimage_mem_nhdsWithin`, `extend_preimage_mem_nhds_of_mem_nhdsWithin`, `extend_prod`, `extend_source`, `extend_source_mem_nhds`, `extend_source_mem_nhdsWithin`, `extend_symm_continuousWithinAt_comp_right_iff`, `extend_symm_preimage_inter_range_eventuallyEq`, `extend_symm_preimage_inter_range_eventuallyEq_aux`, `extend_target`, `extend_target'`, `extend_target_eventuallyEq`, `extend_target_mem_nhdsWithin`, `extend_target_subset_range`, `interior_extend_target_subset_interior_range`, `isOpen_extend_preimage`, `isOpen_extend_preimage'`, `isOpen_extend_source`, `isOpen_extend_target`, `map_extend_nhds`, `map_extend_nhdsWithin`, `map_extend_nhdsWithin_eq_image`, `map_extend_nhdsWithin_eq_image_of_subset`, `map_extend_nhds_of_boundaryless`, `map_extend_nhds_of_mem_interior_range`, `map_extend_symm_nhdsWithin`, `map_extend_symm_nhdsWithin_range`, `mapsTo_extend`, `mem_interior_extend_target`, `nhdsWithin_extend_target_eq`, `tendsto_extend_comp_iff`, `contDiffOn_ext_coord_change`, `contDiffWithinAt_ext_coord_change`, `continuousAt_extChartAt`, `continuousAt_extChartAt'`, `continuousAt_extChartAt_symm`, `continuousAt_extChartAt_symm'`, `continuousAt_extChartAt_symm''`, `continuousOn_extChartAt`, `continuousOn_extChartAt_symm`, `extChartAt_coe`, `extChartAt_coe_symm`, `extChartAt_comp`, `extChartAt_image_nhds_mem_nhds_of_boundaryless`, `extChartAt_image_nhds_mem_nhds_of_mem_interior_range`, `extChartAt_mem_closure_interior`, `extChartAt_model_space_eq_id`, `extChartAt_preimage_inter_eq`, `extChartAt_preimage_mem_nhds`, `extChartAt_preimage_mem_nhds'`, `extChartAt_preimage_mem_nhdsWithin`, `extChartAt_preimage_mem_nhdsWithin'`, `extChartAt_preimage_mem_nhds_of_mem_nhdsWithin`, `extChartAt_prod`, `extChartAt_self_apply`, `extChartAt_self_eq`, `extChartAt_source`, `extChartAt_source_mem_nhds`, `extChartAt_source_mem_nhds'`, `extChartAt_source_mem_nhdsWithin`, `extChartAt_source_mem_nhdsWithin'`, `extChartAt_target`, `extChartAt_target_eventuallyEq`, `extChartAt_target_eventuallyEq'`, `extChartAt_target_eventuallyEq_of_mem`, `extChartAt_target_mem_nhds`, `extChartAt_target_mem_nhds'`, `extChartAt_target_mem_nhdsWithin`, `extChartAt_target_mem_nhdsWithin'`, `extChartAt_target_mem_nhdsWithin_of_mem`, `extChartAt_target_subset_closure_interior`, `extChartAt_target_subset_range`, `extChartAt_target_union_compl_range_mem_nhds_of_mem`, `extChartAt_to_inv`, `ext_chart_model_space_apply`, `ext_coord_change_source`, `interior_extChartAt_target_nonempty`, `isOpen_extChartAt_preimage`, `isOpen_extChartAt_preimage'`, `isOpen_extChartAt_source`, `isOpen_extChartAt_target`, `map_extChartAt_nhds`, `map_extChartAt_nhds'`, `map_extChartAt_nhdsWithin`, `map_extChartAt_nhdsWithin'`, `map_extChartAt_nhdsWithin_eq_image`, `map_extChartAt_nhdsWithin_eq_image'`, `map_extChartAt_nhds_of_boundaryless`, `map_extChartAt_symm_nhdsWithin`, `map_extChartAt_symm_nhdsWithin'`, `map_extChartAt_symm_nhdsWithin_range`, `map_extChartAt_symm_nhdsWithin_range'`, `mapsTo_extChartAt`, `mem_extChartAt_source`, `mem_extChartAt_target`, `nhdsWithin_extChartAt_target_eq`, `nhdsWithin_extChartAt_target_eq'`, `nhdsWithin_extChartAt_target_eq_of_mem`, `uniqueDiffOn_extChartAt_target`, `uniqueDiffWithinAt_extChartAt_target`, `writtenInExtChartAt_chartAt`, `writtenInExtChartAt_chartAt_comp`, `writtenInExtChartAt_chartAt_symm`, `writtenInExtChartAt_chartAt_symm_comp`, `writtenInExtChartAt_extChartAt`, `writtenInExtChartAt_extChartAt_symm`, `writtenInExtChart_prod`	135
Total	138

ContinuousWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`extChartAt_symm_preimage_inter_range_eventuallyEq` 📖	mathematical	`ContinuousWithinAt`	`Filter.EventuallyEq` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PartialEquiv.toFun` `extChartAt` `Set` `Set.instInter` `Set.preimage` `PartialEquiv.symm` `Set.range` `ModelWithCorners.toFun'` `PartialEquiv.target` `PartialEquiv.source`	—	`nhdsWithin_eq_iff_eventuallyEq` `nhdsWithin_extChartAt_symm_preimage_inter_range`
`nhdsWithin_extChartAt_symm_preimage_inter_range` 📖	mathematical	`ContinuousWithinAt`	`nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PartialEquiv.toFun` `extChartAt` `Set` `Set.instInter` `Set.preimage` `PartialEquiv.symm` `Set.range` `ModelWithCorners.toFun'` `PartialEquiv.target` `PartialEquiv.source`	—	`PartialEquiv.image_source_inter_eq'` `map_extChartAt_nhdsWithin_eq_image` `map_extChartAt_nhdsWithin` `nhdsWithin_inter_of_mem'` `extChartAt_source_mem_nhds`

FiniteDimensional

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_locallyCompact_manifold` 📖	mathematical	—	`FiniteDimensional` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`LocallyCompactSpace.of_locallyCompact_manifold` `of_locallyCompactSpace`

LocallyCompactSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_locallyCompact_manifold` 📖	mathematical	—	`LocallyCompactSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`interior_extChartAt_target_nonempty` `interior_subset` `local_compact_nhds` `IsOpen.mem_nhds` `isOpen_extChartAt_source` `PartialEquiv.map_target` `IsCompact.image_of_continuousOn` `ContinuousOn.mono` `continuousOn_extChartAt` `IsCompact.locallyCompactSpace_of_mem_nhds_of_addGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `PartialEquiv.right_inv` `extChartAt_image_nhds_mem_nhds_of_mem_interior_range` `interior_mono` `extChartAt_target_subset_range`

Manifold

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`locallyCompact_of_finiteDimensional` 📖	mathematical	—	`LocallyCompactSpace`	—	`FiniteDimensional.proper` `ModelWithCorners.locallyCompactSpace` `locallyCompact_of_proper` `ChartedSpace.locallyCompactSpace`

OpenPartialHomeomorph

Definitions

Name	Category	Theorems
`extend` 📖	CompOp	76 math math: `map_extend_nhdsWithin_eq_image`, `extend_source_mem_nhds`, `contMDiffAt_extend`, `extend_preimage_inter_eq`, `isOpen_extend_preimage`, `Manifold.IsImmersionAtOfComplement.target_subset_preimage_target`, `map_extend_nhds_of_boundaryless`, `Manifold.IsImmersionAt.map_target_subset_target`, `mdifferentiableWithinAt_iff_of_mem_maximalAtlas`, `tendsto_extend_comp_iff`, `map_extend_nhdsWithin_eq_image_of_subset`, `contMDiffWithinAt_iff_image`, `mem_interior_extend_target`, `extend_target_mem_nhdsWithin`, `isOpen_extend_source`, `Manifold.IsImmersionAtOfComplement.map_target_subset_target`, `IccLeftChart_extend_interior_pos`, `extend_image_target_mem_nhds`, `Manifold.IsImmersionAt.writtenInCharts`, `TangentBundle.trivializationAt_apply`, `contDiffOn_extend_coord_change`, `continuousWithinAt_writtenInExtend_iff`, `continuousAt_extend`, `map_extend_symm_nhdsWithin`, `extend_target`, `contDiffWithinAt_extend_coord_change'`, `mdifferentiableWithinAt_iff_image`, `extend_coord_change_source_mem_nhdsWithin'`, `continuousOn_extend_symm`, `extend_left_inv`, `extend_coe_symm`, `contMDiffOn_iff_of_mem_maximalAtlas'`, `map_extend_nhds`, `extend_symm_preimage_inter_range_eventuallyEq_aux`, `continuousOn_writtenInExtend_iff`, `contMDiffWithinAt_iff_source_of_mem_maximalAtlas`, `extend_image_source_inter`, `IccLeftChart_extend_bot`, `extend_preimage_mem_nhds`, `tangentBundleCore_coordChange`, `contDiffOn_fderiv_coord_change`, `extend_target_eventuallyEq`, `extend_target'`, `extend_prod`, `isOpen_extend_preimage'`, `IccRightChart_extend_top_mem_frontier`, `extend_image_nhds_mem_nhds_of_boundaryless`, `contMDiffOn_iff_source_of_mem_maximalAtlas`, `mdifferentiableOn_iff_of_mem_maximalAtlas'`, `mdifferentiableWithinAt_iff_source_of_mem_maximalAtlas`, `interior_extend_target_subset_interior_range`, `iccLeftChart_extend_zero`, `extend_source`, `extend_coe`, `extend_symm_continuousWithinAt_comp_right_iff`, `contMDiffOn_iff_of_mem_maximalAtlas`, `Manifold.IsImmersionAt.target_subset_preimage_target`, `map_extend_nhdsWithin`, `nhdsWithin_extend_target_eq`, `contMDiffWithinAt_iff_of_mem_maximalAtlas`, `Manifold.IsImmersionAtOfComplement.writtenInCharts`, `isOpen_extend_target`, `continuousAt_extend_symm`, `extend_preimage_mem_nhdsWithin`, `contMDiffOn_extend_symm`, `extend_source_mem_nhdsWithin`, `extend_left_inv'`, `extend_target_subset_range`, `continuousOn_extend`, `map_extend_symm_nhdsWithin_range`, `extend_coord_change_source`, `extend_symm_preimage_inter_range_eventuallyEq`, `IccRightChart_extend_top`, `mapsTo_extend`, `mdifferentiableOn_iff_of_mem_maximalAtlas`, `IccLeftChart_extend_bot_mem_frontier`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`contDiffOn_extend_coord_change` 📖	mathematical	`OpenPartialHomeomorph` `Set` `Set.instMembership` `IsManifold.maximalAtlas`	`ContDiffOn` `PartialEquiv.toFun` `extend` `PartialEquiv.symm` `PartialEquiv.source` `PartialEquiv.trans`	—	`extend_coord_change_source` `ModelWithCorners.image_eq` `StructureGroupoid.compatible_of_mem_maximalAtlas`
`contDiffWithinAt_extend_coord_change` 📖	mathematical	`OpenPartialHomeomorph` `Set` `Set.instMembership` `IsManifold.maximalAtlas` `PartialEquiv.source` `PartialEquiv.trans` `PartialEquiv.symm` `extend`	`ContDiffWithinAt` `PartialEquiv.toFun` `Set.range` `ModelWithCorners.toFun'`	—	`ContDiffWithinAt.mono_of_mem_nhdsWithin` `contDiffOn_extend_coord_change` `extend_coord_change_source` `ModelWithCorners.image_mem_nhdsWithin` `IsOpen.mem_nhds` `open_source`
`contDiffWithinAt_extend_coord_change'` 📖	mathematical	`OpenPartialHomeomorph` `Set` `Set.instMembership` `IsManifold.maximalAtlas` `PartialEquiv.source` `toPartialEquiv`	`ContDiffWithinAt` `PartialEquiv.toFun` `extend` `PartialEquiv.symm` `Set.range` `ModelWithCorners.toFun'`	—	`contDiffWithinAt_extend_coord_change` `extend_image_source_inter` `Set.mem_image_of_mem`
`continuousAt_extend` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `toPartialEquiv`	`ContinuousAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PartialEquiv.toFun` `extend`	—	`ContinuousOn.continuousAt` `continuousOn_extend` `extend_source_mem_nhds`
`continuousAt_extend_symm` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `toPartialEquiv`	`ContinuousAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PartialEquiv.toFun` `PartialEquiv.symm` `extend`	—	`continuousAt_extend_symm'` `PartialEquiv.map_source` `extend_source`
`continuousAt_extend_symm'` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.target` `extend`	`ContinuousAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PartialEquiv.toFun` `PartialEquiv.symm`	—	`ContinuousAt.comp` `continuousAt_symm` `Continuous.continuousAt` `ModelWithCorners.continuous_symm`
`continuousOn_extend` 📖	mathematical	—	`ContinuousOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PartialEquiv.toFun` `extend` `PartialEquiv.source`	—	`Continuous.comp_continuousOn` `ModelWithCorners.continuous` `extend_source` `continuousOn`
`continuousOn_extend_symm` 📖	mathematical	—	`ContinuousOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PartialEquiv.toFun` `PartialEquiv.symm` `extend` `PartialEquiv.target`	—	`ContinuousAt.continuousWithinAt` `continuousAt_extend_symm'`
`continuousOn_writtenInExtend_iff` 📖	mathematical	`Set` `Set.instHasSubset` `PartialEquiv.source` `toPartialEquiv` `Set.MapsTo`	`ContinuousOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PartialEquiv.toFun` `extend` `PartialEquiv.symm` `Set.image`	—	`Set.forall_mem_image` `continuousWithinAt_congr_set` `nhdsWithin_eq_iff_eventuallyEq` `map_extend_nhdsWithin_eq_image_of_subset` `map_extend_nhdsWithin` `continuousWithinAt_writtenInExtend_iff`
`continuousWithinAt_writtenInExtend_iff` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `toPartialEquiv` `Set.MapsTo`	`ContinuousWithinAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PartialEquiv.toFun` `extend` `PartialEquiv.symm` `Set.instInter` `Set.preimage` `Set.range` `ModelWithCorners.toFun'`	—	`extend_left_inv` `tendsto_extend_comp_iff` `map_extend_nhdsWithin` `Filter.eventually_map` `Filter.mp_mem` `inter_mem_nhdsWithin` `IsOpen.mem_nhds` `open_source` `Filter.univ_mem'` `map_extend_symm_nhdsWithin` `Filter.tendsto_map'_iff`
`extend_coe` 📖	mathematical	—	`PartialEquiv.toFun` `extend` `ModelWithCorners.toFun'` `toFun'`	—	—
`extend_coe_symm` 📖	mathematical	—	`PartialEquiv.toFun` `PartialEquiv.symm` `extend` `toFun'` `symm` `ModelWithCorners.symm`	—	—
`extend_coord_change_source` 📖	mathematical	—	`PartialEquiv.source` `PartialEquiv.trans` `PartialEquiv.symm` `extend` `Set.image` `ModelWithCorners.toFun'` `toPartialEquiv` `trans` `symm`	—	`ModelWithCorners.image_eq` `extend_source` `extend_target` `Set.inter_right_comm`
`extend_coord_change_source_mem_nhdsWithin` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `PartialEquiv.trans` `PartialEquiv.symm` `extend`	`Filter` `Filter.instMembership` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set.range` `ModelWithCorners.toFun'`	—	`extend_coord_change_source` `ModelWithCorners.image_mem_nhdsWithin` `IsOpen.mem_nhds` `open_source`
`extend_coord_change_source_mem_nhdsWithin'` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `toPartialEquiv`	`Filter` `Filter.instMembership` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PartialEquiv.toFun` `extend` `Set.range` `ModelWithCorners.toFun'` `PartialEquiv.trans` `PartialEquiv.symm`	—	`extend_coord_change_source_mem_nhdsWithin` `extend_image_source_inter` `Set.mem_image_of_mem`
`extend_image_nhds_mem_nhds_of_boundaryless` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `toPartialEquiv` `Filter` `Filter.instMembership` `nhds`	`UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PartialEquiv.toFun` `extend` `Set.image`	—	`map_extend_nhds_of_boundaryless` `Filter.mem_map` `Filter.mp_mem` `Filter.univ_mem'` `Set.subset_preimage_image`
`extend_image_nhds_mem_nhds_of_mem_interior_range` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `toPartialEquiv` `interior` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set.range` `ModelWithCorners.toFun'` `PartialEquiv.toFun` `extend` `Filter` `Filter.instMembership` `nhds`	`Set.image`	—	`map_extend_nhds_of_mem_interior_range` `Filter.mem_map` `Filter.mp_mem` `Filter.univ_mem'` `Set.subset_preimage_image`
`extend_image_source_inter` 📖	mathematical	—	`Set.image` `PartialEquiv.toFun` `extend` `Set` `Set.instInter` `PartialEquiv.source` `toPartialEquiv` `PartialEquiv.trans` `PartialEquiv.symm`	—	`extend_coord_change_source` `Set.image_congr` `extend_coe` `Set.image_comp` `trans_source''`
`extend_image_target_mem_nhds` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `toPartialEquiv`	`Filter` `Filter.instMembership` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PartialEquiv.toFun` `extend` `Set.range` `ModelWithCorners.toFun'` `Set.image` `PartialEquiv.target`	—	`map_extend_nhds` `Filter.mem_map` `extend_coe` `Set.preimage_comp` `ModelWithCorners.preimage_image` `ContinuousAt.preimage_mem_nhds` `continuousAt` `IsOpen.mem_nhds` `open_target` `map_source`
`extend_left_inv` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `toPartialEquiv`	`PartialEquiv.toFun` `PartialEquiv.symm` `extend`	—	`PartialEquiv.left_inv` `extend_source`
`extend_left_inv'` 📖	mathematical	`Set` `Set.instHasSubset` `PartialEquiv.source` `toPartialEquiv`	`Set.image` `PartialEquiv.toFun` `PartialEquiv.symm` `extend`	—	`Set.EqOn.image_eq_self` `extend_left_inv`
`extend_preimage_inter_eq` 📖	mathematical	—	`Set` `Set.instInter` `Set.preimage` `PartialEquiv.toFun` `PartialEquiv.symm` `extend` `Set.range` `ModelWithCorners.toFun'`	—	`Set.ext`
`extend_preimage_mem_nhds` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `toPartialEquiv` `Filter` `Filter.instMembership` `nhds`	`UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PartialEquiv.toFun` `extend` `Set.preimage` `PartialEquiv.symm`	—	`ContinuousAt.preimage_mem_nhds` `continuousAt_extend_symm` `PartialEquiv.left_inv` `extend_source`
`extend_preimage_mem_nhdsWithin` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `toPartialEquiv` `Filter` `Filter.instMembership` `nhdsWithin`	`UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PartialEquiv.toFun` `extend` `Set.instInter` `Set.preimage` `PartialEquiv.symm` `Set.range` `ModelWithCorners.toFun'`	—	`Filter.mem_map` `map_extend_symm_nhdsWithin`
`extend_preimage_mem_nhds_of_mem_nhdsWithin` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `toPartialEquiv` `Filter` `Filter.instMembership` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PartialEquiv.toFun` `extend` `Set.range` `ModelWithCorners.toFun'`	`nhds` `Set.preimage`	—	`map_extend_nhds`
`extend_prod` 📖	mathematical	—	`extend` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `instTopologicalSpaceProd` `prod` `ModelWithCorners.prod` `PartialEquiv.prod`	—	`PartialEquiv.prod_trans`
`extend_source` 📖	mathematical	—	`PartialEquiv.source` `extend` `toPartialEquiv`	—	`extend.eq_1` `PartialEquiv.trans_source` `ModelWithCorners.source_eq` `Set.preimage_univ` `Set.inter_univ`
`extend_source_mem_nhds` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `toPartialEquiv`	`Filter` `Filter.instMembership` `nhds` `extend`	—	`IsOpen.mem_nhds` `isOpen_extend_source` `extend_source`
`extend_source_mem_nhdsWithin` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `toPartialEquiv`	`Filter` `Filter.instMembership` `nhdsWithin` `extend`	—	`mem_nhdsWithin_of_mem_nhds` `extend_source_mem_nhds`
`extend_symm_continuousWithinAt_comp_right_iff` 📖	mathematical	—	`ContinuousWithinAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PartialEquiv.toFun` `PartialEquiv.symm` `extend` `Set` `Set.instInter` `Set.preimage` `Set.range` `ModelWithCorners.toFun'` `toFun'` `symm`	—	`ModelWithCorners.symm_continuousWithinAt_comp_right_iff`
`extend_symm_preimage_inter_range_eventuallyEq` 📖	mathematical	`Set` `Set.instHasSubset` `PartialEquiv.source` `toPartialEquiv` `Set.instMembership`	`Filter.EventuallyEq` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PartialEquiv.toFun` `extend` `Set.instInter` `Set.preimage` `PartialEquiv.symm` `Set.range` `ModelWithCorners.toFun'` `Set.image`	—	`nhdsWithin_eq_iff_eventuallyEq` `map_extend_nhdsWithin` `map_extend_nhdsWithin_eq_image_of_subset`
`extend_symm_preimage_inter_range_eventuallyEq_aux` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `toPartialEquiv`	`Filter.EventuallyEq` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PartialEquiv.toFun` `extend` `Set.instInter` `Set.preimage` `PartialEquiv.symm` `Set.range` `ModelWithCorners.toFun'` `PartialEquiv.target`	—	`extend_target` `Set.inter_assoc` `Set.inter_comm` `Set.univ_inter` `Filter.EventuallyEq.inter` `Filter.EventuallyEq.symm` `Filter.eventuallyEq_univ` `ContinuousAt.preimage_mem_nhds` `ModelWithCorners.continuousAt_symm` `IsOpen.mem_nhds` `open_target` `extend_coe` `ModelWithCorners.left_inv` `mapsTo` `Filter.EventuallyEq.rfl`
`extend_target` 📖	mathematical	—	`PartialEquiv.target` `extend` `Set` `Set.instInter` `Set.preimage` `PartialEquiv.toFun` `ModelWithCorners.symm` `toPartialEquiv` `Set.range` `ModelWithCorners.toFun'`	—	`ModelWithCorners.target_eq` `Set.inter_comm`
`extend_target'` 📖	mathematical	—	`PartialEquiv.target` `extend` `Set.image` `ModelWithCorners.toFun'` `toPartialEquiv`	—	`extend.eq_1` `PartialEquiv.trans_target''` `ModelWithCorners.source_eq` `Set.univ_inter` `ModelWithCorners.toPartialEquiv_coe`
`extend_target_eventuallyEq` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `toPartialEquiv`	`Filter.EventuallyEq` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PartialEquiv.toFun` `extend` `PartialEquiv.target` `Set.range` `ModelWithCorners.toFun'`	—	`nhdsWithin_eq_iff_eventuallyEq` `nhdsWithin_extend_target_eq`
`extend_target_mem_nhdsWithin` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `toPartialEquiv`	`Filter` `Filter.instMembership` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PartialEquiv.toFun` `extend` `Set.range` `ModelWithCorners.toFun'` `PartialEquiv.target`	—	`PartialEquiv.image_source_eq_target` `map_extend_nhds` `Filter.image_mem_map` `extend_source_mem_nhds`
`extend_target_subset_range` 📖	mathematical	—	`Set` `Set.instHasSubset` `PartialEquiv.target` `extend` `Set.range` `ModelWithCorners.toFun'`	—	`ModelWithCorners.target_eq`
`interior_extend_target_subset_interior_range` 📖	mathematical	—	`Set` `Set.instHasSubset` `interior` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PartialEquiv.target` `extend` `Set.range` `ModelWithCorners.toFun'`	—	`extend_target` `interior_inter` `IsOpen.interior_eq` `IsOpen.preimage` `ModelWithCorners.continuous_symm` `open_target` `Set.inter_subset_right`
`isOpen_extend_preimage` 📖	mathematical	`IsOpen` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`Set` `Set.instInter` `PartialEquiv.source` `toPartialEquiv` `Set.preimage` `PartialEquiv.toFun` `extend`	—	`extend_source` `isOpen_extend_preimage'`
`isOpen_extend_preimage'` 📖	mathematical	`IsOpen` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`Set` `Set.instInter` `PartialEquiv.source` `extend` `Set.preimage` `PartialEquiv.toFun`	—	`ContinuousOn.isOpen_inter_preimage` `continuousOn_extend` `isOpen_extend_source`
`isOpen_extend_source` 📖	mathematical	—	`IsOpen` `PartialEquiv.source` `extend`	—	`extend_source` `open_source`
`isOpen_extend_target` 📖	mathematical	—	`IsOpen` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PartialEquiv.target` `extend`	—	`extend_target` `ModelWithCorners.range_eq_univ` `Set.inter_univ` `Continuous.isOpen_preimage` `ModelWithCorners.continuous_symm` `open_target`
`map_extend_nhds` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `toPartialEquiv`	`Filter.map` `PartialEquiv.toFun` `extend` `nhds` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set.range` `ModelWithCorners.toFun'`	—	`extend_coe` `ModelWithCorners.map_nhds_eq` `map_nhds_eq` `Filter.map_map`
`map_extend_nhdsWithin` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `toPartialEquiv`	`Filter.map` `PartialEquiv.toFun` `extend` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set.instInter` `Set.preimage` `PartialEquiv.symm` `Set.range` `ModelWithCorners.toFun'`	—	`map_extend_nhdsWithin_eq_image` `nhdsWithin_inter` `nhdsWithin_extend_target_eq` `PartialEquiv.image_source_inter_eq'` `Set.inter_comm`
`map_extend_nhdsWithin_eq_image` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `toPartialEquiv`	`Filter.map` `PartialEquiv.toFun` `extend` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set.image` `Set.instInter`	—	`nhdsWithin_inter_of_mem` `extend_source_mem_nhdsWithin` `Set.LeftInvOn.map_nhdsWithin_eq` `Set.LeftInvOn.mono` `PartialEquiv.leftInvOn` `Set.inter_subset_left` `PartialEquiv.left_inv` `extend_source` `ContinuousAt.continuousWithinAt` `continuousAt_extend_symm` `continuousAt_extend`
`map_extend_nhdsWithin_eq_image_of_subset` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `toPartialEquiv` `Set.instHasSubset`	`Filter.map` `PartialEquiv.toFun` `extend` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set.image`	—	`map_extend_nhdsWithin_eq_image` `Set.inter_eq_self_of_subset_right` `extend_source`
`map_extend_nhds_of_boundaryless` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `toPartialEquiv`	`Filter.map` `PartialEquiv.toFun` `extend` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`map_extend_nhds` `ModelWithCorners.range_eq_univ` `nhdsWithin_univ`
`map_extend_nhds_of_mem_interior_range` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `toPartialEquiv` `interior` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set.range` `ModelWithCorners.toFun'` `PartialEquiv.toFun` `extend`	`Filter.map` `nhds`	—	`map_extend_nhds` `nhdsWithin_eq_nhds` `Filter.mem_of_superset` `IsOpen.mem_nhds` `isOpen_interior` `interior_subset`
`map_extend_symm_nhdsWithin` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `toPartialEquiv`	`Filter.map` `PartialEquiv.toFun` `PartialEquiv.symm` `extend` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set.instInter` `Set.preimage` `Set.range` `ModelWithCorners.toFun'`	—	`map_extend_nhdsWithin` `Filter.map_map` `Filter.map_congr` `Set.EqOn.eventuallyEq_of_mem` `Set.LeftInvOn.eqOn` `PartialEquiv.leftInvOn` `extend_source_mem_nhdsWithin` `Filter.map_id`
`map_extend_symm_nhdsWithin_range` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `toPartialEquiv`	`Filter.map` `PartialEquiv.toFun` `PartialEquiv.symm` `extend` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set.range` `ModelWithCorners.toFun'` `nhds`	—	`nhdsWithin_univ` `map_extend_symm_nhdsWithin` `Set.preimage_univ` `Set.univ_inter`
`mapsTo_extend` 📖	mathematical	`Set` `Set.instHasSubset` `PartialEquiv.source` `toPartialEquiv`	`Set.MapsTo` `PartialEquiv.toFun` `extend` `Set.instInter` `Set.preimage` `PartialEquiv.symm` `Set.range` `ModelWithCorners.toFun'`	—	`Set.mapsTo_iff_image_subset` `extend_coe` `extend_coe_symm` `Set.preimage_comp` `ModelWithCorners.image_eq` `Set.image_comp` `image_eq_target_inter_inv_preimage` `Set.image_mono` `Set.inter_subset_right`
`mem_interior_extend_target` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.target` `toPartialEquiv` `interior` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set.range` `ModelWithCorners.toFun'`	`extend`	—	`extend_target` `interior_inter` `IsOpen.interior_eq` `IsOpen.preimage` `ModelWithCorners.continuous_symm` `open_target` `Set.mem_inter_iff` `Set.mem_preimage` `Set.mem_of_eq_of_mem` `ModelWithCorners.left_inv`
`nhdsWithin_extend_target_eq` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `toPartialEquiv`	`nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PartialEquiv.toFun` `extend` `PartialEquiv.target` `Set.range` `ModelWithCorners.toFun'`	—	`LE.le.antisymm` `nhdsWithin_mono` `extend_target_subset_range` `nhdsWithin_le_of_mem` `extend_target_mem_nhdsWithin`
`tendsto_extend_comp_iff` 📖	mathematical	`Filter.Eventually` `Set` `Set.instMembership` `PartialEquiv.source` `toPartialEquiv`	`Filter.Tendsto` `PartialEquiv.toFun` `extend` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`Filter.mem_map` `Filter.Tendsto.comp` `ContinuousAt.tendsto` `continuousAt_extend_symm` `Filter.mp_mem` `extend_left_inv` `Filter.univ_mem'` `continuousAt_extend`

(root)

Definitions

Name	Category	Theorems
`extChartAt` 📖	CompOp	158 math math: `contMDiffAt_iff_of_mem_source`, `contMDiffWithinAt_iff_target`, `SmoothBumpFunction.support_eq_symm_image`, `extChartAt_to_inv`, `isOpen_extChartAt_preimage'`, `MDifferentiableWithinAt.differentiableWithinAt_mpullbackWithin_vectorField`, `SmoothBumpFunction.rOut_pos`, `mdifferentiableOn_iff`, `mdifferentiable_iff_target`, `contMDiffAt_iff_source`, `eventually_enorm_mfderivWithin_symm_extChartAt_lt`, `extChartAt_target_eventuallyEq`, `TangentBundle.symmL_trivializationAt`, `ContinuousWithinAt.extChartAt_symm_preimage_inter_range_eventuallyEq`, `map_extChartAt_symm_nhdsWithin`, `mdifferentiableOn_extChartAt`, `mdifferentiableWithinAt_iff_target_inter`, `tangentCoordChange_def`, `continuousAt_extChartAt`, `isOpen_extChartAt_target`, `hasMFDerivAt_extChartAt`, `extChartAt_preimage_inter_eq`, `map_extChartAt_symm_nhdsWithin_range`, `extChartAt_inl_apply`, `SmoothBumpCovering.mem_extChartAt_source_of_eq_one`, `inTangentCoordinates_eq_mfderiv_comp`, `mdifferentiableAt_iff`, `MDifferentiableWithinAt.differentiableWithinAt_writtenInExtChartAt`, `SmoothBumpFunction.exists_r_pos_lt_subset_ball`, `extChartAt_target_mem_nhdsWithin`, `eventually_norm_mfderivWithin_symm_extChartAt_lt`, `UniqueMDiffOn.uniqueDiffOn_target_inter`, `extChartAt_self_apply`, `mapsTo_extChartAt`, `continuousOn_tangentCoordChange`, `preimage_extChartAt_eventuallyEq_compl_singleton`, `mdifferentiableOn_iff_target`, `hasMFDerivWithinAt_extChartAt`, `UniqueMDiffOn.uniqueMDiffOn_target_inter`, `contMDiffAt_iff_source_of_mem_source`, `SmoothBumpFunction.support_eq_inter_preimage`, `SmoothBumpFunction.tsupport_subset_symm_image_closedBall`, `MDifferentiableAt.differentiableWithinAt_writtenInExtChartAt`, `mem_extChartAt_target`, `map_extChartAt_nhds_of_boundaryless`, `extChartAt_preimage_mem_nhds`, `extChartAt_self_eq`, `continuousOn_extChartAt`, `contMDiffWithinAt_iff_of_mem_source'`, `SmoothBumpFunction.ball_subset`, `contMDiff_iff_target`, `mdifferentiableOn_extChartAt_symm`, `SmoothBumpFunction.eqOn_source`, `VectorField.mlieBracketWithin_def`, `contMDiffOn_extChartAt`, `extChartAt_inr_apply`, `isOpen_extChartAt_preimage`, `mdifferentiable_iff`, `contMDiffAt_iff`, `isOpen_extChartAt_source`, `extChartAt_preimage_mem_nhdsWithin`, `contMDiffOn_extChartAt_symm`, `contMDiffWithinAt_extChartAt_symm_range_self`, `extChartAt_source`, `contMDiffWithinAt_iff_target_of_mem_source`, `mdifferentiableOn_iff_of_subset_source`, `ext_coord_change_source`, `mem_extChartAt_source`, `MDifferentiableAt.mfderiv`, `ContinuousWithinAt.nhdsWithin_extChartAt_symm_preimage_inter_range`, `MDifferentiableWithinAt.mfderivWithin`, `contMDiffWithinAt_iff`, `extChartAt_source_mem_nhds`, `FiberBundle.extChartAt`, `SmoothBumpFunction.isClosed_image_of_isClosed`, `extChartAt_image_nhds_mem_nhds_of_boundaryless`, `SmoothBumpFunction.isClosed_symm_image_closedBall`, `extChartAt_target_subset_range`, `mdifferentiableWithinAt_iff'`, `TangentBundle.continuousLinearMapAt_trivializationAt`, `mdifferentiableAt_iff_target_of_mem_source`, `ext_chart_model_space_apply`, `SmoothBumpFunction.eventuallyEq_of_mem_source`, `continuousAt_extChartAt_symm`, `contMDiffAt_iff_target_of_mem_source`, `contMDiffWithinAt_iff'`, `ModelWithCorners.coe_extChartAt_transContinuousLinearEquiv_symm`, `uniqueMDiffWithinAt_iff`, `VectorField.eventuallyEq_mpullback_mpullbackWithin_extChartAt`, `extChartAt_model_space_eq_id`, `map_extChartAt_nhdsWithin`, `eventually_enorm_mfderiv_extChartAt_lt`, `contMDiffOn_iff`, `UniqueMDiffOn.uniqueDiffOn_inter_preimage`, `mdifferentiableWithinAt_iff_target_inter'`, `contMDiffWithinAt_extChartAt_symm_target_self`, `contMDiff_iff`, `SmoothBumpCovering.mem_extChartAt_ind_source`, `uniqueMDiffWithinAt_iff_inter_range`, `continuousOn_extChartAt_symm`, `contDiffOn_ext_coord_change`, `mdifferentiableWithinAt_iff_of_mem_source'`, `VectorField.contMDiffWithinAt_mpullbackWithin_extChartAt_symm`, `mdifferentiableWithinAt_iff`, `eventually_riemannianEDist_le_edist_extChartAt`, `contMDiffAt_extChartAt`, `extChartAt_source_mem_nhdsWithin`, `SmoothBumpFunction.coe_def`, `FiberBundle.extChartAt_target`, `contMDiffWithinAt_iff_source`, `nhdsWithin_extChartAt_target_eq`, `contMDiffWithinAt_iff_source_of_mem_source`, `contMDiffOn_iff_of_subset_source`, `ModelWithCorners.isInteriorPoint_iff`, `mdifferentiableAt_iff_source_of_mem_source`, `mdifferentiableAt_iff_of_mem_source`, `interior_extChartAt_target_nonempty`, `mdifferentiableWithinAt_iff_target_of_mem_source`, `map_extChartAt_nhdsWithin_eq_image`, `eventually_norm_mfderivWithin_symm_extChartAt_comp_lt`, `SmoothBumpFunction.tsupport_subset_extChartAt_source`, `extChartAt_target`, `mdifferentiableWithinAt_iff_source_of_mem_source`, `mdifferentiableAt_iff_target`, `contMDiffAt_extChartAt'`, `extChartAt_coe_symm`, `extChartAt_comp`, `ModelWithCorners.coe_extChartAt_transContinuousLinearEquiv`, `mdifferentiableWithinAt_iff_of_mem_source`, `VectorField.mlieBracketWithin_apply`, `VectorField.eventually_contMDiffWithinAt_mpullbackWithin_extChartAt_symm`, `SmoothBumpFunction.nhdsWithin_range_basis`, `contMDiffOn_iff_target`, `uniqueDiffOn_extChartAt_target`, `extChartAt_target_mem_nhds`, `contMDiffAt_iff_target`, `writtenInExtChartAt_sumInr_eventuallyEq_id`, `SmoothBumpCovering.embeddingPiTangent_coe`, `range_mem_nhds_isInteriorPoint`, `uniqueDiffWithinAt_extChartAt_target`, `ModelWithCorners.isBoundaryPoint_iff`, `eventually_norm_mfderiv_extChartAt_lt`, `extChartAt_coe`, `writtenInExtChartAt_sumInl_eventuallyEq_id`, `mdifferentiableAt_extChartAt`, `writtenInExtChartAt_comp`, `map_extChartAt_nhds`, `mdifferentiableWithinAt_iff_target`, `contMDiffWithinAt_iff_of_mem_source`, `IsMIntegralCurveAt.eventually_hasDerivAt`, `extChartAt_prod`, `SmoothBumpFunction.image_eq_inter_preimage_of_subset_support`, `extChartAt_target_subset_closure_interior`, `SmoothBumpFunction.closedBall_subset`, `tangentBundleCore_coordChange_achart`, `SmoothBumpFunction.isCompact_symm_image_closedBall`, `SmoothBumpFunction.ball_inter_range_eq_ball_inter_target`, `ModelWithCorners.extChartAt_transContinuousLinearEquiv_target`
`writtenInExtChartAt` 📖	CompOp	21 math math: `writtenInExtChartAt_chartAt`, `mdifferentiableWithinAt_iff_target_inter`, `mdifferentiableAt_iff`, `MDifferentiableWithinAt.differentiableWithinAt_writtenInExtChartAt`, `writtenInExtChart_prod`, `MDifferentiableAt.differentiableWithinAt_writtenInExtChartAt`, `FiberBundle.writtenInExtChartAt_trivializationAt`, `writtenInExtChartAt_model_space`, `MDifferentiableAt.mfderiv`, `MDifferentiableWithinAt.mfderivWithin`, `writtenInExtChartAt_chartAt_comp`, `mdifferentiableWithinAt_iff'`, `writtenInExtChartAt_extChartAt`, `writtenInExtChartAt_extChartAt_symm`, `writtenInExtChartAt_sumSwap_eventuallyEq_id`, `FiberBundle.writtenInExtChartAt_trivializationAt_symm`, `writtenInExtChartAt_chartAt_symm_comp`, `writtenInExtChartAt_chartAt_symm`, `writtenInExtChartAt_sumInr_eventuallyEq_id`, `writtenInExtChartAt_sumInl_eventuallyEq_id`, `writtenInExtChartAt_comp`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`contDiffOn_ext_coord_change` 📖	mathematical	—	`ContDiffOn` `PartialEquiv.toFun` `extChartAt` `PartialEquiv.symm` `PartialEquiv.source` `PartialEquiv.trans`	—	`OpenPartialHomeomorph.contDiffOn_extend_coord_change` `IsManifold.chart_mem_maximalAtlas`
`contDiffWithinAt_ext_coord_change` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `PartialEquiv.trans` `PartialEquiv.symm` `extChartAt`	`ContDiffWithinAt` `PartialEquiv.toFun` `Set.range` `ModelWithCorners.toFun'`	—	`OpenPartialHomeomorph.contDiffWithinAt_extend_coord_change` `IsManifold.chart_mem_maximalAtlas`
`continuousAt_extChartAt` 📖	mathematical	—	`ContinuousAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PartialEquiv.toFun` `extChartAt`	—	`continuousAt_extChartAt'` `mem_extChartAt_source`
`continuousAt_extChartAt'` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `extChartAt`	`ContinuousAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PartialEquiv.toFun`	—	`OpenPartialHomeomorph.continuousAt_extend` `extChartAt_source`
`continuousAt_extChartAt_symm` 📖	mathematical	—	`ContinuousAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PartialEquiv.toFun` `PartialEquiv.symm` `extChartAt`	—	`continuousAt_extChartAt_symm'` `mem_extChartAt_source`
`continuousAt_extChartAt_symm'` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `extChartAt`	`ContinuousAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PartialEquiv.toFun` `PartialEquiv.symm`	—	`continuousAt_extChartAt_symm''` `PartialEquiv.map_source`
`continuousAt_extChartAt_symm''` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.target` `extChartAt`	`ContinuousAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PartialEquiv.toFun` `PartialEquiv.symm`	—	`OpenPartialHomeomorph.continuousAt_extend_symm'`
`continuousOn_extChartAt` 📖	mathematical	—	`ContinuousOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PartialEquiv.toFun` `extChartAt` `PartialEquiv.source`	—	`OpenPartialHomeomorph.continuousOn_extend`
`continuousOn_extChartAt_symm` 📖	mathematical	—	`ContinuousOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PartialEquiv.toFun` `PartialEquiv.symm` `extChartAt` `PartialEquiv.target`	—	`ContinuousAt.continuousWithinAt` `continuousAt_extChartAt_symm''`
`extChartAt_coe` 📖	mathematical	—	`PartialEquiv.toFun` `extChartAt` `ModelWithCorners.toFun'` `OpenPartialHomeomorph.toFun'` `chartAt`	—	—
`extChartAt_coe_symm` 📖	mathematical	—	`PartialEquiv.toFun` `PartialEquiv.symm` `extChartAt` `OpenPartialHomeomorph.toFun'` `OpenPartialHomeomorph.symm` `chartAt` `ModelWithCorners.symm`	—	—
`extChartAt_comp` 📖	mathematical	—	`extChartAt` `ChartedSpace.comp` `PartialEquiv.trans` `OpenPartialHomeomorph.toPartialEquiv` `chartAt` `OpenPartialHomeomorph.toFun'`	—	`PartialEquiv.trans_assoc`
`extChartAt_image_nhds_mem_nhds_of_boundaryless` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds`	`UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PartialEquiv.toFun` `extChartAt` `Set.image`	—	`extChartAt.eq_1` `OpenPartialHomeomorph.extend_image_nhds_mem_nhds_of_boundaryless` `mem_chart_source`
`extChartAt_image_nhds_mem_nhds_of_mem_interior_range` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `extChartAt` `interior` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set.range` `ModelWithCorners.toFun'` `PartialEquiv.toFun` `Filter` `Filter.instMembership` `nhds`	`Set.image`	—	`extChartAt.eq_1` `OpenPartialHomeomorph.extend_image_nhds_mem_nhds_of_mem_interior_range` `ModelWithCorners.source_eq` `Set.inter_univ`
`extChartAt_mem_closure_interior` 📖	mathematical	`Set` `Set.instMembership` `closure` `interior` `PartialEquiv.source` `extChartAt`	`UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set.instInter` `Set.preimage` `PartialEquiv.toFun` `PartialEquiv.symm` `PartialEquiv.target`	—	`interior_inter` `ContinuousAt.preimage_mem_nhds` `continuousAt_extChartAt'` `IsOpen.mem_nhds` `mem_closure_iff_nhds` `Filter.inter_mem` `isOpen_extChartAt_source` `continuousAt_extChartAt_symm'` `PartialEquiv.left_inv` `mem_interior_iff_mem_nhds` `extChartAt_target_subset_closure_interior` `PartialEquiv.map_source`
`extChartAt_model_space_eq_id` 📖	mathematical	—	`extChartAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `PartialEquiv.refl`	—	`PartialEquiv.trans_refl`
`extChartAt_preimage_inter_eq` 📖	mathematical	—	`Set` `Set.instInter` `Set.preimage` `PartialEquiv.toFun` `PartialEquiv.symm` `extChartAt` `Set.range` `ModelWithCorners.toFun'`	—	`Set.ext`
`extChartAt_preimage_mem_nhds` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds`	`UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PartialEquiv.toFun` `extChartAt` `Set.preimage` `PartialEquiv.symm`	—	`ContinuousAt.preimage_mem_nhds` `continuousAt_extChartAt_symm` `PartialEquiv.left_inv` `mem_extChartAt_source`
`extChartAt_preimage_mem_nhds'` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `extChartAt` `Filter` `Filter.instMembership` `nhds`	`UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PartialEquiv.toFun` `Set.preimage` `PartialEquiv.symm`	—	`OpenPartialHomeomorph.extend_preimage_mem_nhds` `extChartAt_source`
`extChartAt_preimage_mem_nhdsWithin` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhdsWithin`	`UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PartialEquiv.toFun` `extChartAt` `Set.instInter` `Set.preimage` `PartialEquiv.symm` `Set.range` `ModelWithCorners.toFun'`	—	`extChartAt_preimage_mem_nhdsWithin'` `mem_extChartAt_source`
`extChartAt_preimage_mem_nhdsWithin'` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `extChartAt` `Filter` `Filter.instMembership` `nhdsWithin`	`UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PartialEquiv.toFun` `Set.instInter` `Set.preimage` `PartialEquiv.symm` `Set.range` `ModelWithCorners.toFun'`	—	`Filter.mem_map` `map_extChartAt_symm_nhdsWithin'`
`extChartAt_preimage_mem_nhds_of_mem_nhdsWithin` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `extChartAt` `Filter` `Filter.instMembership` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PartialEquiv.toFun` `Set.range` `ModelWithCorners.toFun'`	`nhds` `Set.preimage`	—	`OpenPartialHomeomorph.extend_preimage_mem_nhds_of_mem_nhdsWithin` `ModelWithCorners.source_eq` `Set.inter_univ`
`extChartAt_prod` 📖	mathematical	—	`extChartAt` `ModelProd` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `instTopologicalSpaceModelProd` `instTopologicalSpaceProd` `ModelWithCorners.prod` `prodChartedSpace` `PartialEquiv.prod`	—	`PartialEquiv.prod_trans`
`extChartAt_self_apply` 📖	mathematical	—	`PartialEquiv.toFun` `extChartAt` `chartedSpaceSelf` `ModelWithCorners.toFun'`	—	—
`extChartAt_self_eq` 📖	mathematical	—	`PartialEquiv.toFun` `extChartAt` `chartedSpaceSelf` `ModelWithCorners.toFun'`	—	—
`extChartAt_source` 📖	mathematical	—	`PartialEquiv.source` `extChartAt` `OpenPartialHomeomorph.toPartialEquiv` `chartAt`	—	`OpenPartialHomeomorph.extend_source`
`extChartAt_source_mem_nhds` 📖	mathematical	—	`Set` `Filter` `Filter.instMembership` `nhds` `PartialEquiv.source` `extChartAt`	—	`extChartAt_source_mem_nhds'` `mem_extChartAt_source`
`extChartAt_source_mem_nhds'` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `extChartAt`	`Filter` `Filter.instMembership` `nhds`	—	`OpenPartialHomeomorph.extend_source_mem_nhds` `extChartAt_source`
`extChartAt_source_mem_nhdsWithin` 📖	mathematical	—	`Set` `Filter` `Filter.instMembership` `nhdsWithin` `PartialEquiv.source` `extChartAt`	—	`mem_nhdsWithin_of_mem_nhds` `extChartAt_source_mem_nhds`
`extChartAt_source_mem_nhdsWithin'` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `extChartAt`	`Filter` `Filter.instMembership` `nhdsWithin`	—	`mem_nhdsWithin_of_mem_nhds` `extChartAt_source_mem_nhds'`
`extChartAt_target` 📖	mathematical	—	`PartialEquiv.target` `extChartAt` `Set` `Set.instInter` `Set.preimage` `PartialEquiv.toFun` `ModelWithCorners.symm` `OpenPartialHomeomorph.toPartialEquiv` `chartAt` `Set.range` `ModelWithCorners.toFun'`	—	`OpenPartialHomeomorph.extend_target`
`extChartAt_target_eventuallyEq` 📖	mathematical	—	`Filter.EventuallyEq` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PartialEquiv.toFun` `extChartAt` `PartialEquiv.target` `Set.range` `ModelWithCorners.toFun'`	—	`nhdsWithin_eq_iff_eventuallyEq` `nhdsWithin_extChartAt_target_eq`
`extChartAt_target_eventuallyEq'` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `extChartAt`	`Filter.EventuallyEq` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PartialEquiv.toFun` `PartialEquiv.target` `Set.range` `ModelWithCorners.toFun'`	—	`nhdsWithin_eq_iff_eventuallyEq` `nhdsWithin_extChartAt_target_eq'`
`extChartAt_target_eventuallyEq_of_mem` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.target` `extChartAt`	`Filter.EventuallyEq` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set.range` `ModelWithCorners.toFun'`	—	`nhdsWithin_eq_iff_eventuallyEq` `nhdsWithin_extChartAt_target_eq_of_mem`
`extChartAt_target_mem_nhds` 📖	mathematical	—	`Set` `Filter` `Filter.instMembership` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PartialEquiv.toFun` `extChartAt` `PartialEquiv.target`	—	`ModelWithCorners.range_eq_univ` `nhdsWithin_univ` `extChartAt_target_mem_nhdsWithin`
`extChartAt_target_mem_nhds'` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.target` `extChartAt`	`Filter` `Filter.instMembership` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`IsOpen.mem_nhds` `isOpen_extChartAt_target`
`extChartAt_target_mem_nhdsWithin` 📖	mathematical	—	`Set` `Filter` `Filter.instMembership` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PartialEquiv.toFun` `extChartAt` `Set.range` `ModelWithCorners.toFun'` `PartialEquiv.target`	—	`extChartAt_target_mem_nhdsWithin'` `mem_extChartAt_source`
`extChartAt_target_mem_nhdsWithin'` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `extChartAt`	`Filter` `Filter.instMembership` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PartialEquiv.toFun` `Set.range` `ModelWithCorners.toFun'` `PartialEquiv.target`	—	`OpenPartialHomeomorph.extend_target_mem_nhdsWithin` `extChartAt_source`
`extChartAt_target_mem_nhdsWithin_of_mem` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.target` `extChartAt`	`Filter` `Filter.instMembership` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set.range` `ModelWithCorners.toFun'`	—	`PartialEquiv.right_inv` `extChartAt_target_mem_nhdsWithin'` `PartialEquiv.map_target`
`extChartAt_target_subset_closure_interior` 📖	mathematical	—	`Set` `Set.instHasSubset` `PartialEquiv.target` `extChartAt` `closure` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `interior`	—	`mem_closure_iff_nhds` `Filter.inter_mem` `extChartAt_target_union_compl_range_mem_nhds_of_mem` `ModelWithCorners.range_subset_closure_interior` `extChartAt_target_subset_range` `ModelWithCorners.target_eq` `interior_subset` `Filter.EventuallyEq.mem_interior` `Filter.EventuallyEq.symm` `extChartAt_target_eventuallyEq_of_mem`
`extChartAt_target_subset_range` 📖	mathematical	—	`Set` `Set.instHasSubset` `PartialEquiv.target` `extChartAt` `Set.range` `ModelWithCorners.toFun'`	—	`ModelWithCorners.target_eq`
`extChartAt_target_union_compl_range_mem_nhds_of_mem` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.target` `extChartAt`	`Filter` `Filter.instMembership` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set.instUnion` `Compl.compl` `Set.instCompl` `Set.range` `ModelWithCorners.toFun'`	—	`nhdsWithin_univ` `Set.union_compl_self` `nhdsWithin_union` `Filter.union_mem_sup` `extChartAt_target_mem_nhdsWithin_of_mem` `self_mem_nhdsWithin`
`extChartAt_to_inv` 📖	mathematical	—	`PartialEquiv.toFun` `PartialEquiv.symm` `extChartAt`	—	`PartialEquiv.left_inv` `mem_extChartAt_source`
`ext_chart_model_space_apply` 📖	mathematical	—	`PartialEquiv.toFun` `extChartAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf`	—	—
`ext_coord_change_source` 📖	mathematical	—	`PartialEquiv.source` `PartialEquiv.trans` `PartialEquiv.symm` `extChartAt` `Set.image` `ModelWithCorners.toFun'` `OpenPartialHomeomorph.toPartialEquiv` `OpenPartialHomeomorph.trans` `OpenPartialHomeomorph.symm` `chartAt`	—	`OpenPartialHomeomorph.extend_coord_change_source`
`interior_extChartAt_target_nonempty` 📖	mathematical	—	`Set.Nonempty` `interior` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PartialEquiv.target` `extChartAt`	—	`extChartAt_target_subset_closure_interior` `mem_extChartAt_target` `closure_empty`
`isOpen_extChartAt_preimage` 📖	mathematical	`IsOpen` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`Set` `Set.instInter` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv` `chartAt` `Set.preimage` `PartialEquiv.toFun` `extChartAt`	—	`extChartAt_source` `isOpen_extChartAt_preimage'`
`isOpen_extChartAt_preimage'` 📖	mathematical	`IsOpen` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`Set` `Set.instInter` `PartialEquiv.source` `extChartAt` `Set.preimage` `PartialEquiv.toFun`	—	`OpenPartialHomeomorph.isOpen_extend_preimage'`
`isOpen_extChartAt_source` 📖	mathematical	—	`IsOpen` `PartialEquiv.source` `extChartAt`	—	`OpenPartialHomeomorph.isOpen_extend_source`
`isOpen_extChartAt_target` 📖	mathematical	—	`IsOpen` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PartialEquiv.target` `extChartAt`	—	`extChartAt_target` `ModelWithCorners.range_eq_univ` `Set.inter_univ` `IsOpen.preimage` `ModelWithCorners.continuous_symm` `OpenPartialHomeomorph.open_target`
`map_extChartAt_nhds` 📖	mathematical	—	`Filter.map` `PartialEquiv.toFun` `extChartAt` `nhds` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set.range` `ModelWithCorners.toFun'`	—	`map_extChartAt_nhds'` `mem_extChartAt_source`
`map_extChartAt_nhds'` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `extChartAt`	`Filter.map` `PartialEquiv.toFun` `nhds` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set.range` `ModelWithCorners.toFun'`	—	`OpenPartialHomeomorph.map_extend_nhds` `extChartAt_source`
`map_extChartAt_nhdsWithin` 📖	mathematical	—	`Filter.map` `PartialEquiv.toFun` `extChartAt` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set` `Set.instInter` `Set.preimage` `PartialEquiv.symm` `Set.range` `ModelWithCorners.toFun'`	—	`map_extChartAt_nhdsWithin'` `mem_extChartAt_source`
`map_extChartAt_nhdsWithin'` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `extChartAt`	`Filter.map` `PartialEquiv.toFun` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set.instInter` `Set.preimage` `PartialEquiv.symm` `Set.range` `ModelWithCorners.toFun'`	—	`OpenPartialHomeomorph.map_extend_nhdsWithin` `extChartAt_source`
`map_extChartAt_nhdsWithin_eq_image` 📖	mathematical	—	`Filter.map` `PartialEquiv.toFun` `extChartAt` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set.image` `Set` `Set.instInter` `PartialEquiv.source`	—	`map_extChartAt_nhdsWithin_eq_image'` `mem_extChartAt_source`
`map_extChartAt_nhdsWithin_eq_image'` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `extChartAt`	`Filter.map` `PartialEquiv.toFun` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set.image` `Set.instInter`	—	`OpenPartialHomeomorph.map_extend_nhdsWithin_eq_image` `extChartAt_source`
`map_extChartAt_nhds_of_boundaryless` 📖	mathematical	—	`Filter.map` `PartialEquiv.toFun` `extChartAt` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`extChartAt.eq_1` `OpenPartialHomeomorph.map_extend_nhds_of_boundaryless` `mem_chart_source`
`map_extChartAt_symm_nhdsWithin` 📖	mathematical	—	`Filter.map` `PartialEquiv.toFun` `PartialEquiv.symm` `extChartAt` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set` `Set.instInter` `Set.preimage` `Set.range` `ModelWithCorners.toFun'`	—	`map_extChartAt_symm_nhdsWithin'` `mem_extChartAt_source`
`map_extChartAt_symm_nhdsWithin'` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `extChartAt`	`Filter.map` `PartialEquiv.toFun` `PartialEquiv.symm` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set.instInter` `Set.preimage` `Set.range` `ModelWithCorners.toFun'`	—	`OpenPartialHomeomorph.map_extend_symm_nhdsWithin` `extChartAt_source`
`map_extChartAt_symm_nhdsWithin_range` 📖	mathematical	—	`Filter.map` `PartialEquiv.toFun` `PartialEquiv.symm` `extChartAt` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set.range` `ModelWithCorners.toFun'` `nhds`	—	`map_extChartAt_symm_nhdsWithin_range'` `mem_extChartAt_source`
`map_extChartAt_symm_nhdsWithin_range'` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `extChartAt`	`Filter.map` `PartialEquiv.toFun` `PartialEquiv.symm` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set.range` `ModelWithCorners.toFun'` `nhds`	—	`OpenPartialHomeomorph.map_extend_symm_nhdsWithin_range` `extChartAt_source`
`mapsTo_extChartAt` 📖	mathematical	`Set` `Set.instHasSubset` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv` `chartAt`	`Set.MapsTo` `PartialEquiv.toFun` `extChartAt` `Set.instInter` `Set.preimage` `PartialEquiv.symm` `Set.range` `ModelWithCorners.toFun'`	—	`OpenPartialHomeomorph.mapsTo_extend`
`mem_extChartAt_source` 📖	mathematical	—	`Set` `Set.instMembership` `PartialEquiv.source` `extChartAt`	—	`extChartAt_source`
`mem_extChartAt_target` 📖	mathematical	—	`Set` `Set.instMembership` `PartialEquiv.target` `extChartAt` `PartialEquiv.toFun`	—	`PartialEquiv.map_source` `mem_extChartAt_source`
`nhdsWithin_extChartAt_target_eq` 📖	mathematical	—	`nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PartialEquiv.toFun` `extChartAt` `PartialEquiv.target` `Set.range` `ModelWithCorners.toFun'`	—	`nhdsWithin_extChartAt_target_eq'` `mem_extChartAt_source`
`nhdsWithin_extChartAt_target_eq'` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `extChartAt`	`nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PartialEquiv.toFun` `PartialEquiv.target` `Set.range` `ModelWithCorners.toFun'`	—	`OpenPartialHomeomorph.nhdsWithin_extend_target_eq` `extChartAt_source`
`nhdsWithin_extChartAt_target_eq_of_mem` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.target` `extChartAt`	`nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set.range` `ModelWithCorners.toFun'`	—	`PartialEquiv.right_inv` `nhdsWithin_extChartAt_target_eq'` `PartialEquiv.map_target`
`uniqueDiffOn_extChartAt_target` 📖	mathematical	—	`UniqueDiffOn` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `PartialEquiv.target` `extChartAt`	—	`extChartAt_target` `ModelWithCorners.uniqueDiffOn_preimage` `OpenPartialHomeomorph.open_target`
`uniqueDiffWithinAt_extChartAt_target` 📖	mathematical	—	`UniqueDiffWithinAt` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `PartialEquiv.target` `extChartAt` `PartialEquiv.toFun`	—	`uniqueDiffOn_extChartAt_target` `mem_extChartAt_target`
`writtenInExtChartAt_chartAt` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.target` `extChartAt`	`writtenInExtChartAt` `chartedSpaceSelf` `OpenPartialHomeomorph.toFun'` `chartAt`	—	`PartialEquiv.refl_trans` `OpenPartialHomeomorph.right_inv` `ModelWithCorners.target_eq` `ModelWithCorners.right_inv`
`writtenInExtChartAt_chartAt_comp` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.target` `extChartAt` `ChartedSpace.comp`	`writtenInExtChartAt` `OpenPartialHomeomorph.toFun'` `chartAt`	—	`OpenPartialHomeomorph.right_inv` `ModelWithCorners.target_eq` `ModelWithCorners.right_inv`
`writtenInExtChartAt_chartAt_symm` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.target` `extChartAt`	`writtenInExtChartAt` `chartedSpaceSelf` `OpenPartialHomeomorph.toFun'` `chartAt` `OpenPartialHomeomorph.symm`	—	`OpenPartialHomeomorph.left_inv` `PartialEquiv.refl_trans` `OpenPartialHomeomorph.right_inv` `ModelWithCorners.target_eq` `ModelWithCorners.right_inv`
`writtenInExtChartAt_chartAt_symm_comp` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.target` `extChartAt` `ChartedSpace.comp`	`writtenInExtChartAt` `OpenPartialHomeomorph.toFun'` `chartAt` `OpenPartialHomeomorph.symm`	—	`OpenPartialHomeomorph.left_inv` `OpenPartialHomeomorph.right_inv` `ModelWithCorners.target_eq` `ModelWithCorners.right_inv`
`writtenInExtChartAt_extChartAt` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.target` `extChartAt`	`writtenInExtChartAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `PartialEquiv.toFun`	—	`PartialEquiv.trans_refl` `OpenPartialHomeomorph.right_inv` `ModelWithCorners.target_eq` `ModelWithCorners.right_inv`
`writtenInExtChartAt_extChartAt_symm` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.target` `extChartAt`	`writtenInExtChartAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `PartialEquiv.toFun` `PartialEquiv.symm`	—	`ModelWithCorners.left_inv` `OpenPartialHomeomorph.left_inv` `PartialEquiv.trans_refl` `OpenPartialHomeomorph.right_inv` `ModelWithCorners.target_eq` `ModelWithCorners.right_inv`
`writtenInExtChart_prod` 📖	mathematical	—	`writtenInExtChartAt` `ModelProd` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `instTopologicalSpaceModelProd` `instTopologicalSpaceProd` `ModelWithCorners.prod` `prodChartedSpace`	—	`PartialEquiv.prod_symm`

---

← Back to Index