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` 📖	mathematical	`ContMDiff`	`ContMDiff`	—	`contMDiffOn_univ` `ContMDiffOn.comp` `Set.subset_preimage_univ`
`comp_contMDiffOn` 📖	mathematical	`ContMDiff` `ContMDiffOn`	`ContMDiffOn`	—	`ContMDiffOn.comp` `contMDiffOn` `Set.subset_preimage_univ`
`extend_one` 📖	mathematical	`HasCompactMulSupport` `TopologicalSpace.Opens` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `instTopologicalSpaceSubtype` `ContMDiff` `TopologicalSpace.Opens.instChartedSpace`	`ContMDiff` `Function.extend` `TopologicalSpace.Opens` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `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`	`ContMDiff` `Function.extend` `TopologicalSpace.Opens` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `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`	`ContMDiff` `Nat.iterate`	—	`contMDiffOn_univ` `ContMDiffOn.iterate` `Set.mapsTo_univ`
`of_comp_isOpenEmbedding` 📖	mathematical	`Topology.IsOpenEmbedding` `ContMDiff` `chartedSpaceSelf`	`ContMDiff` `Topology.IsOpenEmbedding.singletonChartedSpace`	—	`Topology.IsOpenEmbedding.toOpenPartialHomeomorph_left_inv` `ContMDiffOn.comp_contMDiff` `contMDiffOn_isOpenEmbedding_symm`
`piecewise` 📖	mathematical	`ContMDiff` `Filter.EventuallyEq` `nhds`	`ContMDiff` `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`	`ContMDiff` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `Real.pseudoMetricSpace` `chartedSpaceSelf` `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` 📖	mathematical	`ContMDiffAt`	`ContMDiffAt`	—	`ContMDiffWithinAt.comp` `Set.mapsTo_univ`
`comp_contMDiffWithinAt` 📖	mathematical	`ContMDiffAt` `ContMDiffWithinAt`	`ContMDiffWithinAt`	—	`ContMDiffWithinAt.comp` `Set.mapsTo_univ`
`comp_contMDiffWithinAt_of_eq` 📖	mathematical	`ContMDiffAt` `ContMDiffWithinAt`	`ContMDiffWithinAt`	—	`comp_contMDiffWithinAt`
`comp_of_eq` 📖	mathematical	`ContMDiffAt`	`ContMDiffAt`	—	`comp`

ContMDiffOn

Theorems

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

ContMDiffWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	mathematical	`ContMDiffWithinAt` `Set.MapsTo`	`ContMDiffWithinAt`	—	`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`	`ContMDiffWithinAt` `Set` `Set.instInter` `Set.preimage`	—	`comp` `mono` `Set.inter_subset_left` `Set.inter_subset_right`
`comp_of_eq` 📖	mathematical	`ContMDiffWithinAt` `Set.MapsTo`	`ContMDiffWithinAt`	—	`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` `TopologicalSpace.Opens` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `instTopologicalSpaceSubtype` `TopologicalSpace.Opens.instChartedSpace` `TopologicalSpace.Opens.inclusion`	—	`StructureGroupoid.LocalInvariantProp.liftProp_inclusion` `contDiffWithinAt_localInvariantProp` `contDiffWithinAtProp_id`
`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