Atlas

📁 Source: Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean

Statistics

Metric	Count
Definitions	0
Theorems contMDiffAt_extChartAt, contMDiffAt_extChartAt', contMDiffAt_extend, contMDiffAt_of_mem_maximalAtlas, contMDiffAt_symm_of_mem_maximalAtlas, contMDiffOn_chart, contMDiffOn_chart_symm, contMDiffOn_extChartAt, contMDiffOn_extChartAt_symm, contMDiffOn_extend_symm, contMDiffOn_model_symm, contMDiffOn_of_mem_contDiffGroupoid, contMDiffOn_of_mem_maximalAtlas, contMDiffOn_symm_of_mem_maximalAtlas, contMDiffWithinAt_extChartAt_symm_range, contMDiffWithinAt_extChartAt_symm_range_self, contMDiffWithinAt_extChartAt_symm_target, contMDiffWithinAt_extChartAt_symm_target_self, contMDiff_model, isLocalStructomorphOn_contDiffGroupoid_iff, isLocalStructomorphOn_contDiffGroupoid_iff_aux	21
Total	21

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contMDiffAt_extChartAt 📖	mathematical	—	ContMDiffAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf PartialEquiv.toFun extChartAt	—	contMDiffAt_iff_source ContMDiffWithinAt.congr_of_eventuallyEq_of_mem contMDiffWithinAt_id Filter.mp_mem extChartAt_target_mem_nhdsWithin Filter.univ_mem' PartialEquiv.right_inv
contMDiffAt_extChartAt' 📖	mathematical	Set Set.instMembership PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv chartAt	ContMDiffAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf PartialEquiv.toFun extChartAt	—	contMDiffAt_extend IsManifold.chart_mem_maximalAtlas
contMDiffAt_extend 📖	mathematical	OpenPartialHomeomorph Set Set.instMembership IsManifold.maximalAtlas PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv	ContMDiffAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf PartialEquiv.toFun OpenPartialHomeomorph.extend	—	ContMDiffAt.comp contMDiff_model contMDiffAt_of_mem_maximalAtlas
contMDiffAt_of_mem_maximalAtlas 📖	mathematical	OpenPartialHomeomorph Set Set.instMembership IsManifold.maximalAtlas PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv	ContMDiffAt chartedSpaceSelf OpenPartialHomeomorph.toFun'	—	ContMDiffOn.contMDiffAt contMDiffOn_of_mem_maximalAtlas IsOpen.mem_nhds OpenPartialHomeomorph.open_source
contMDiffAt_symm_of_mem_maximalAtlas 📖	mathematical	OpenPartialHomeomorph Set Set.instMembership IsManifold.maximalAtlas PartialEquiv.target OpenPartialHomeomorph.toPartialEquiv	ContMDiffAt chartedSpaceSelf OpenPartialHomeomorph.toFun' OpenPartialHomeomorph.symm	—	ContMDiffOn.contMDiffAt contMDiffOn_symm_of_mem_maximalAtlas IsOpen.mem_nhds OpenPartialHomeomorph.open_target
contMDiffOn_chart 📖	mathematical	—	ContMDiffOn chartedSpaceSelf OpenPartialHomeomorph.toFun' chartAt PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv	—	contMDiffOn_of_mem_maximalAtlas IsManifold.chart_mem_maximalAtlas
contMDiffOn_chart_symm 📖	mathematical	—	ContMDiffOn chartedSpaceSelf OpenPartialHomeomorph.toFun' OpenPartialHomeomorph.symm chartAt PartialEquiv.target OpenPartialHomeomorph.toPartialEquiv	—	contMDiffOn_symm_of_mem_maximalAtlas IsManifold.chart_mem_maximalAtlas
contMDiffOn_extChartAt 📖	mathematical	—	ContMDiffOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf PartialEquiv.toFun extChartAt PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv chartAt	—	ContMDiffAt.contMDiffWithinAt contMDiffAt_extChartAt'
contMDiffOn_extChartAt_symm 📖	mathematical	—	ContMDiffOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf PartialEquiv.toFun PartialEquiv.symm extChartAt PartialEquiv.target	—	extChartAt_target ModelWithCorners.image_eq contMDiffOn_extend_symm IsManifold.chart_mem_maximalAtlas
contMDiffOn_extend_symm 📖	mathematical	OpenPartialHomeomorph Set Set.instMembership IsManifold.maximalAtlas	ContMDiffOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf PartialEquiv.toFun PartialEquiv.symm OpenPartialHomeomorph.extend Set.image ModelWithCorners.toFun' PartialEquiv.target OpenPartialHomeomorph.toPartialEquiv	—	ContMDiffOn.comp contMDiffOn_symm_of_mem_maximalAtlas ContMDiffOn.mono contMDiffOn_model_symm Set.image_subset_range Set.preimage_preimage ModelWithCorners.left_inv subset_refl Set.instReflSubset
contMDiffOn_model_symm 📖	mathematical	—	ContMDiffOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf PartialEquiv.toFun ModelWithCorners.symm Set.range ModelWithCorners.toFun'	—	contMDiffOn_iff IsManifold.instOfTopWithTopENat instIsManifoldModelSpace ModelWithCorners.continuousOn_symm PartialEquiv.refl_trans PartialEquiv.trans_refl ModelWithCorners.source_eq Set.inter_univ Set.univ_inter ContDiffOn.congr contDiffOn_id ModelWithCorners.right_inv
contMDiffOn_of_mem_contDiffGroupoid 📖	mathematical	OpenPartialHomeomorph StructureGroupoid instMembershipOpenPartialHomeomorphStructureGroupoid contDiffGroupoid	ContMDiffOn chartedSpaceSelf OpenPartialHomeomorph.toFun' PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv	—	StructureGroupoid.LocalInvariantProp.liftPropOn_of_mem_groupoid contDiffWithinAt_localInvariantProp contDiffWithinAtProp_id
contMDiffOn_of_mem_maximalAtlas 📖	mathematical	OpenPartialHomeomorph Set Set.instMembership IsManifold.maximalAtlas	ContMDiffOn chartedSpaceSelf OpenPartialHomeomorph.toFun' PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv	—	StructureGroupoid.LocalInvariantProp.liftPropOn_of_mem_maximalAtlas IsManifold.toHasGroupoid contDiffWithinAt_localInvariantProp contDiffWithinAtProp_id
contMDiffOn_symm_of_mem_maximalAtlas 📖	mathematical	OpenPartialHomeomorph Set Set.instMembership IsManifold.maximalAtlas	ContMDiffOn chartedSpaceSelf OpenPartialHomeomorph.toFun' OpenPartialHomeomorph.symm PartialEquiv.target OpenPartialHomeomorph.toPartialEquiv	—	StructureGroupoid.LocalInvariantProp.liftPropOn_symm_of_mem_maximalAtlas IsManifold.toHasGroupoid contDiffWithinAt_localInvariantProp contDiffWithinAtProp_id
contMDiffWithinAt_extChartAt_symm_range 📖	mathematical	Set Set.instMembership PartialEquiv.target extChartAt	ContMDiffWithinAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf PartialEquiv.toFun PartialEquiv.symm Set.range ModelWithCorners.toFun'	—	ContMDiffWithinAt.mono_of_mem_nhdsWithin contMDiffWithinAt_extChartAt_symm_target extChartAt_target_mem_nhdsWithin_of_mem
contMDiffWithinAt_extChartAt_symm_range_self 📖	mathematical	—	ContMDiffWithinAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf PartialEquiv.toFun PartialEquiv.symm extChartAt Set.range ModelWithCorners.toFun'	—	ContMDiffWithinAt.mono_of_mem_nhdsWithin contMDiffWithinAt_extChartAt_symm_target_self extChartAt_target_mem_nhdsWithin
contMDiffWithinAt_extChartAt_symm_target 📖	mathematical	Set Set.instMembership PartialEquiv.target extChartAt	ContMDiffWithinAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf PartialEquiv.toFun PartialEquiv.symm	—	contMDiffOn_extChartAt_symm
contMDiffWithinAt_extChartAt_symm_target_self 📖	mathematical	—	ContMDiffWithinAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf PartialEquiv.toFun PartialEquiv.symm extChartAt PartialEquiv.target	—	contMDiffWithinAt_iff_target ContinuousAt.continuousWithinAt ContinuousAt.comp OpenPartialHomeomorph.continuousAt ModelWithCorners.left_inv ModelWithCorners.continuousAt_symm ContMDiffWithinAt.congr_of_mem contMDiffWithinAt_id OpenPartialHomeomorph.left_inv PartialEquiv.right_inv ModelWithCorners.target_eq
contMDiff_model 📖	mathematical	—	ContMDiff chartedSpaceSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf ModelWithCorners.toFun'	—	contMDiffAt_iff ModelWithCorners.continuousAt PartialEquiv.trans_refl PartialEquiv.refl_trans ContDiffWithinAt.congr_of_eventuallyEq contDiffWithinAt_id Filter.eventuallyEq_of_mem self_mem_nhdsWithin ModelWithCorners.right_inv ModelWithCorners.left_inv
isLocalStructomorphOn_contDiffGroupoid_iff 📖	mathematical	—	ChartedSpace.LiftPropOn StructureGroupoid.IsLocalStructomorphWithinAt contDiffGroupoid OpenPartialHomeomorph.toFun' PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv ContMDiffOn OpenPartialHomeomorph.symm PartialEquiv.target	—	isLocalStructomorphOn_contDiffGroupoid_iff_aux OpenPartialHomeomorph.mapsTo ContinuousAt.continuousWithinAt OpenPartialHomeomorph.continuousAt OpenPartialHomeomorph.right_inv OpenPartialHomeomorph.left_inv OpenPartialHomeomorph.isLocalStructomorphWithinAt_iff' instClosedUnderRestrictionContDiffGroupoid Set.EqOn.symm OpenPartialHomeomorph.IsImage.symm_eqOn_of_inter_eq_of_eqOn OpenPartialHomeomorph.isImage_source_target Set.inter_self Set.inter_eq_right HasSubset.Subset.trans Set.instIsTransSubset StructureGroupoid.symm ContMDiffWithinAt.continuousWithinAt ContMDiffWithinAt.mono ModelWithCorners.right_inv ContDiffWithinAt.mono contMDiffWithinAt_iff_of_mem_source Set.eqOn_refl
isLocalStructomorphOn_contDiffGroupoid_iff_aux 📖	mathematical	ChartedSpace.LiftPropOn StructureGroupoid.IsLocalStructomorphWithinAt contDiffGroupoid OpenPartialHomeomorph.toFun' PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv	ContMDiffOn	—	contMDiffOn_of_locally_contMDiffOn OpenPartialHomeomorph.left_inv IsOpen.inter OpenPartialHomeomorph.open_source contMDiffOn_chart_symm contMDiffOn_of_mem_contDiffGroupoid contMDiffOn_chart ContMDiffOn.mono ContMDiffOn.comp' ContMDiffOn.congr

---

← Back to Index