Basic

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

Statistics

Metric	Count
Definitions	0
Theorems comp, comp_contMDiffOn, extend_one, extend_zero, iterate, of_comp_isOpenEmbedding, piecewise, piecewise_Iic, comp, comp_contMDiffWithinAt, comp_contMDiffWithinAt_of_eq, comp_of_eq, comp, comp', comp_contMDiff, iUnion_of_isOpen, iterate, union_of_isOpen, comp, comp', comp_of_eq, contMDiffAt_const, contMDiffAt_id, contMDiffAt_of_notMem, contMDiffAt_of_notMem_mulTSupport, contMDiffAt_of_subsingleton, contMDiffAt_one, contMDiffAt_subtype_iff, contMDiffAt_zero, contMDiffOn_const, contMDiffOn_iUnion_iff_of_isOpen, contMDiffOn_id, contMDiffOn_isOpenEmbedding_symm, contMDiffOn_of_subsingleton, contMDiffOn_one, contMDiffOn_union_iff_of_isOpen, contMDiffOn_zero, contMDiffWithinAt_const, contMDiffWithinAt_id, contMDiffWithinAt_of_notMem, contMDiffWithinAt_of_notMem_mulTSupport, contMDiffWithinAt_of_subsingleton, contMDiffWithinAt_one, contMDiffWithinAt_zero, contMDiff_const, contMDiff_id, contMDiff_inclusion, contMDiff_isOpenEmbedding, contMDiff_of_contMDiffOn_iUnion_of_isOpen, contMDiff_of_contMDiffOn_union_of_isOpen, contMDiff_of_discreteTopology, contMDiff_of_mulTSupport, contMDiff_of_subsingleton, contMDiff_of_tsupport, contMDiff_one, contMDiff_subtype_val, contMDiff_zero	57
Total	57

ContMDiff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	—	ContMDiff	—	—	contMDiffOn_univ ContMDiffOn.comp Set.subset_preimage_univ
comp_contMDiffOn 📖	—	ContMDiff ContMDiffOn	—	—	ContMDiffOn.comp contMDiffOn Set.subset_preimage_univ
extend_one 📖	mathematical	HasCompactMulSupport TopologicalSpace.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike instTopologicalSpaceSubtype ContMDiff TopologicalSpace.Opens.instChartedSpace	Function.extend Pi.instOne	—	contMDiff_of_mulTSupport CanLift.prf Subtype.canLift Subtype.coe_image_subset HasCompactMulSupport.mulTSupport_extend_one_subset continuous_subtype_val contMDiffAt_subtype_iff Function.extend_comp Subtype.val_injective contMDiffAt
extend_zero 📖	mathematical	HasCompactSupport TopologicalSpace.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike instTopologicalSpaceSubtype ContMDiff TopologicalSpace.Opens.instChartedSpace	Function.extend Pi.instZero	—	contMDiff_of_tsupport CanLift.prf Subtype.canLift Subtype.coe_image_subset HasCompactSupport.tsupport_extend_zero_subset continuous_subtype_val contMDiffAt_subtype_iff Function.extend_comp Subtype.val_injective contMDiffAt
iterate 📖	mathematical	ContMDiff	Nat.iterate	—	contMDiffOn_univ ContMDiffOn.iterate Set.mapsTo_univ
of_comp_isOpenEmbedding 📖	mathematical	Topology.IsOpenEmbedding ContMDiff chartedSpaceSelf	Topology.IsOpenEmbedding.singletonChartedSpace	—	Topology.IsOpenEmbedding.toOpenPartialHomeomorph_left_inv ContMDiffOn.comp_contMDiff contMDiffOn_isOpenEmbedding_symm
piecewise 📖	mathematical	ContMDiff Filter.EventuallyEq nhds	Set.piecewise	—	ContMDiffAt.congr_of_eventuallyEq Filter.mp_mem IsOpen.mem_nhds isOpen_interior Filter.univ_mem' Set.piecewise_eq_of_mem interior_subset IsClosed.isOpen_compl isClosed_closure Set.piecewise_eq_of_notMem Mathlib.Tactic.Contrapose.contrapose₃ subset_closure
piecewise_Iic 📖	mathematical	ContMDiff Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup NormedField.toNormedSpace NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf Real.pseudoMetricSpace chartedSpaceSelf Filter.EventuallyEq nhds	Set.piecewise Set.Iic Real.instPreorder Set.decidableMemIic Real.decidableLE	—	piecewise frontier_Iic' instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial

ContMDiffAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	—	ContMDiffAt	—	—	ContMDiffWithinAt.comp Set.mapsTo_univ
comp_contMDiffWithinAt 📖	—	ContMDiffAt ContMDiffWithinAt	—	—	ContMDiffWithinAt.comp Set.mapsTo_univ
comp_contMDiffWithinAt_of_eq 📖	—	ContMDiffAt ContMDiffWithinAt	—	—	comp_contMDiffWithinAt
comp_of_eq 📖	—	ContMDiffAt	—	—	comp

ContMDiffOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	—	ContMDiffOn Set Set.instHasSubset Set.preimage	—	—	ContMDiffWithinAt.comp
comp' 📖	mathematical	ContMDiffOn	Set Set.instInter Set.preimage	—	comp mono Set.inter_subset_left Set.inter_subset_right
comp_contMDiff 📖	—	ContMDiffOn ContMDiff Set Set.instMembership	—	—	contMDiffOn_univ comp ContMDiff.contMDiffOn
iUnion_of_isOpen 📖	mathematical	ContMDiffOn IsOpen	Set.iUnion	—	ContMDiffAt.contMDiffWithinAt contMDiffAt IsOpen.mem_nhds
iterate 📖	mathematical	ContMDiffOn Set.MapsTo	Nat.iterate	—	contMDiffOn_id comp
union_of_isOpen 📖	mathematical	ContMDiffOn IsOpen	Set Set.instUnion	—	ContMDiffAt.contMDiffWithinAt ContMDiffWithinAt.contMDiffAt IsOpen.mem_nhds

ContMDiffWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	—	ContMDiffWithinAt Set.MapsTo	—	—	contMDiffWithinAt_iff ContinuousWithinAt.comp ModelWithCorners.left_inv OpenPartialHomeomorph.left_inv Filter.mp_mem inter_mem_nhdsWithin extChartAt_source_mem_nhds ContinuousWithinAt.tendsto Filter.univ_mem' PartialEquiv.left_inv ContDiffWithinAt.congr_of_eventuallyEq ContDiffWithinAt.mono_of_mem_nhdsWithin ContDiffWithinAt.comp ContDiffWithinAt.mono Set.inter_subset_right Set.MapsTo.mono_left Set.mapsTo_preimage Set.inter_subset_left Filter.inter_mem Set.mem_range_self self_mem_nhdsWithin
comp' 📖	mathematical	ContMDiffWithinAt	Set Set.instInter Set.preimage	—	comp mono Set.inter_subset_left Set.inter_subset_right
comp_of_eq 📖	—	ContMDiffWithinAt Set.MapsTo	—	—	comp

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contMDiffAt_const 📖	mathematical	—	ContMDiffAt	—	ContMDiff.contMDiffAt contMDiff_const
contMDiffAt_id 📖	mathematical	—	ContMDiffAt	—	ContMDiff.contMDiffAt contMDiff_id
contMDiffAt_of_notMem 📖	mathematical	Set Set.instMembership tsupport	ContMDiffAt	—	contMDiffWithinAt_of_notMem
contMDiffAt_of_notMem_mulTSupport 📖	mathematical	Set Set.instMembership mulTSupport	ContMDiffAt	—	contMDiffWithinAt_of_notMem_mulTSupport
contMDiffAt_of_subsingleton 📖	mathematical	—	ContMDiffAt	—	ContMDiff.contMDiffAt contMDiff_of_subsingleton
contMDiffAt_one 📖	mathematical	—	ContMDiffAt Pi.instOne	—	ContMDiff.contMDiffAt contMDiff_one
contMDiffAt_subtype_iff 📖	mathematical	—	ContMDiffAt TopologicalSpace.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike instTopologicalSpaceSubtype TopologicalSpace.Opens.instChartedSpace	—	StructureGroupoid.LocalInvariantProp.liftPropAt_iff_comp_subtype_val contDiffWithinAt_localInvariantProp
contMDiffAt_zero 📖	mathematical	—	ContMDiffAt Pi.instZero	—	ContMDiff.contMDiffAt contMDiff_zero
contMDiffOn_const 📖	mathematical	—	ContMDiffOn	—	ContMDiff.contMDiffOn contMDiff_const
contMDiffOn_iUnion_iff_of_isOpen 📖	mathematical	IsOpen	ContMDiffOn Set.iUnion	—	ContMDiffOn.mono Set.subset_iUnion_of_subset ContMDiffOn.iUnion_of_isOpen
contMDiffOn_id 📖	mathematical	—	ContMDiffOn	—	ContMDiff.contMDiffOn contMDiff_id
contMDiffOn_isOpenEmbedding_symm 📖	mathematical	Topology.IsOpenEmbedding	ContMDiffOn chartedSpaceSelf Topology.IsOpenEmbedding.singletonChartedSpace OpenPartialHomeomorph.toFun' OpenPartialHomeomorph.symm Topology.IsOpenEmbedding.toOpenPartialHomeomorph Set.range	—	contMDiffOn_iff IsManifold.instOfTopWithTopENat instIsManifoldModelSpace Topology.IsOpenEmbedding.isManifold_singleton Topology.IsOpenEmbedding.toOpenPartialHomeomorph_target OpenPartialHomeomorph.continuousOn_symm ContDiffOn.congr contDiffOn_id PartialEquiv.refl_trans ModelWithCorners.symm.eq_1 Set.mem_preimage Topology.IsOpenEmbedding.toOpenPartialHomeomorph_right_inv ModelWithCorners.right_inv Set.mem_of_subset_of_mem extChartAt_target_subset_range
contMDiffOn_of_subsingleton 📖	mathematical	—	ContMDiffOn	—	ContMDiff.contMDiffOn contMDiff_of_subsingleton
contMDiffOn_one 📖	mathematical	—	ContMDiffOn Pi.instOne	—	ContMDiff.contMDiffOn contMDiff_one
contMDiffOn_union_iff_of_isOpen 📖	mathematical	IsOpen	ContMDiffOn Set Set.instUnion	—	ContMDiffOn.mono Set.subset_union_left Set.subset_union_right ContMDiffOn.union_of_isOpen
contMDiffOn_zero 📖	mathematical	—	ContMDiffOn Pi.instZero	—	ContMDiff.contMDiffOn contMDiff_zero
contMDiffWithinAt_const 📖	mathematical	—	ContMDiffWithinAt	—	ContMDiffAt.contMDiffWithinAt contMDiffAt_const
contMDiffWithinAt_id 📖	mathematical	—	ContMDiffWithinAt	—	ContMDiffAt.contMDiffWithinAt contMDiffAt_id
contMDiffWithinAt_of_notMem 📖	mathematical	Set Set.instMembership tsupport	ContMDiffWithinAt	—	ContMDiffWithinAt.congr_of_eventuallyEq contMDiffWithinAt_const eventually_nhdsWithin_of_eventually_nhds notMem_tsupport_iff_eventuallyEq image_eq_zero_of_notMem_tsupport
contMDiffWithinAt_of_notMem_mulTSupport 📖	mathematical	Set Set.instMembership mulTSupport	ContMDiffWithinAt	—	ContMDiffWithinAt.congr_of_eventuallyEq contMDiffWithinAt_const eventually_nhdsWithin_of_eventually_nhds notMem_mulTSupport_iff_eventuallyEq image_eq_one_of_notMem_mulTSupport
contMDiffWithinAt_of_subsingleton 📖	mathematical	—	ContMDiffWithinAt	—	ContMDiffAt.contMDiffWithinAt contMDiffAt_of_subsingleton
contMDiffWithinAt_one 📖	mathematical	—	ContMDiffWithinAt Pi.instOne	—	ContMDiffAt.contMDiffWithinAt contMDiffAt_const
contMDiffWithinAt_zero 📖	mathematical	—	ContMDiffWithinAt Pi.instZero	—	ContMDiffAt.contMDiffWithinAt contMDiffAt_const
contMDiff_const 📖	mathematical	—	ContMDiff	—	continuousWithinAt_const contDiffWithinAt_const
contMDiff_id 📖	mathematical	—	ContMDiff	—	ContMDiff.of_le StructureGroupoid.LocalInvariantProp.liftProp_id contDiffWithinAt_localInvariantProp contDiffWithinAtProp_id le_top
contMDiff_inclusion 📖	mathematical	TopologicalSpace.Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder	ContMDiff SetLike.instMembership TopologicalSpace.Opens.instSetLike instTopologicalSpaceSubtype TopologicalSpace.Opens.instChartedSpace TopologicalSpace.Opens.inclusion	—	StructureGroupoid.LocalInvariantProp.liftProp_inclusion contDiffWithinAt_localInvariantProp Set.univ_inter ContDiffWithinAt.congr contDiffWithinAt_id ModelWithCorners.rightInvOn ModelWithCorners.left_inv
contMDiff_isOpenEmbedding 📖	mathematical	Topology.IsOpenEmbedding	ContMDiff Topology.IsOpenEmbedding.singletonChartedSpace chartedSpaceSelf	—	contMDiff_iff IsManifold.instOfTopWithTopENat Topology.IsOpenEmbedding.isManifold_singleton instIsManifoldModelSpace Topology.IsOpenEmbedding.continuous ContDiffOn.congr contDiffOn_id PartialEquiv.refl_trans Topology.IsOpenEmbedding.toOpenPartialHomeomorph_right_inv extChartAt_target Topology.IsOpenEmbedding.toOpenPartialHomeomorph_target Topology.IsOpenEmbedding.toOpenPartialHomeomorph_source OpenPartialHomeomorph.singletonChartedSpace_chartAt_eq Set.mem_preimage ModelWithCorners.right_inv Set.mem_of_subset_of_mem extChartAt_target_subset_range
contMDiff_of_contMDiffOn_iUnion_of_isOpen 📖	mathematical	ContMDiffOn IsOpen Set.iUnion Set.univ	ContMDiff	—	contMDiffOn_univ ContMDiffOn.iUnion_of_isOpen
contMDiff_of_contMDiffOn_union_of_isOpen 📖	mathematical	ContMDiffOn Set Set.instUnion Set.univ IsOpen	ContMDiff	—	contMDiffOn_univ ContMDiffOn.union_of_isOpen
contMDiff_of_discreteTopology 📖	mathematical	—	ContMDiff	—	ContMDiffAt.congr_of_eventuallyEq ContMDiff.contMDiffAt contMDiff_const nhds_discrete
contMDiff_of_mulTSupport 📖	mathematical	ContMDiffAt	ContMDiff	—	ContMDiffAt.congr_of_eventuallyEq contMDiffAt_const notMem_mulTSupport_iff_eventuallyEq
contMDiff_of_subsingleton 📖	mathematical	—	ContMDiff	—	contMDiffAt_const
contMDiff_of_tsupport 📖	mathematical	ContMDiffAt	ContMDiff	—	ContMDiffAt.congr_of_eventuallyEq contMDiffAt_const notMem_tsupport_iff_eventuallyEq
contMDiff_one 📖	mathematical	—	ContMDiff Pi.instOne	—	—
contMDiff_subtype_val 📖	mathematical	—	ContMDiff TopologicalSpace.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike instTopologicalSpaceSubtype TopologicalSpace.Opens.instChartedSpace	—	contMDiffAt_subtype_iff contMDiffAt_id
contMDiff_zero 📖	mathematical	—	ContMDiff Pi.instZero	—	contMDiff_const

---

← Back to Index