Constructions

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

Statistics

Metric	Count
Definitions	0
Theorems `along_fst`, `along_snd`, `curry_left`, `curry_right`, `fst`, `inl`, `inr`, `prodMap`, `prodMk`, `prodMk_space`, `snd`, `sumElim`, `sumMap`, `swap`, `along_fst`, `along_snd`, `comp₂`, `comp₂_of_eq`, `curry_left`, `curry_right`, `fst`, `prodMap`, `prodMap'`, `prodMk`, `prodMk_space`, `snd`, `along_fst`, `along_snd`, `curry_left`, `curry_right`, `prodMap`, `prodMk`, `prodMk_space`, `along_fst`, `along_snd`, `comp₂`, `comp₂_of_eq`, `curry_left`, `curry_right`, `fst`, `prodMap`, `prodMap'`, `prodMk`, `prodMk_space`, `snd`, `contMDiffAt_fst`, `contMDiffAt_pi_space`, `contMDiffAt_prod_iff`, `contMDiffAt_prod_module_iff`, `contMDiffAt_snd`, `contMDiffOn_fst`, `contMDiffOn_pi_space`, `contMDiffOn_prod_iff`, `contMDiffOn_prod_module_iff`, `contMDiffOn_snd`, `contMDiffWithinAt_fst`, `contMDiffWithinAt_pi_space`, `contMDiffWithinAt_prod_iff`, `contMDiffWithinAt_prod_module_iff`, `contMDiffWithinAt_snd`, `contMDiff_fst`, `contMDiff_of_contMDiff_inl`, `contMDiff_of_contMDiff_inr`, `contMDiff_pi_space`, `contMDiff_prod_assoc`, `contMDiff_prod_iff`, `contMDiff_prod_module_iff`, `contMDiff_snd`, `contMDiff_sum_map`, `extChartAt_inl_apply`, `extChartAt_inr_apply`	71
Total	71

ContMDiff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`along_fst` 📖	—	`ContMDiff` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	—	—	`curry_left`
`along_snd` 📖	—	`ContMDiff` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	—	—	`curry_right`
`curry_left` 📖	—	`ContMDiff` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	—	—	`ContMDiffAt.along_fst`
`curry_right` 📖	—	`ContMDiff` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	—	—	`ContMDiffAt.along_snd`
`fst` 📖	—	`ContMDiff` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	—	—	`comp` `contMDiff_fst`
`inl` 📖	mathematical	—	`ContMDiff` `instTopologicalSpaceSum` `ChartedSpace.sum`	—	`contMDiffAt_iff` `Continuous.continuousAt` `continuous_inl` `ContDiffWithinAt.congr_of_eventuallyEq` `contDiffWithinAt_id` `ModelWithCorners.image_eq` `OpenPartialHomeomorph.extend_image_target_mem_nhds` `mem_chart_source` `Filter.mp_mem` `Filter.univ_mem'` `nonempty_of_chartedSpace` `Topology.IsOpenEmbedding.inl` `ChartedSpace.sum_chartAt_inl` `OpenPartialHomeomorph.lift_openEmbedding.congr_simp` `Function.Injective.extend_apply` `Sum.inl_injective` `OpenPartialHomeomorph.right_inv` `ModelWithCorners.right_inv` `ModelWithCorners.left_inv` `OpenPartialHomeomorph.left_inv`
`inr` 📖	mathematical	—	`ContMDiff` `instTopologicalSpaceSum` `ChartedSpace.sum`	—	`contMDiffAt_iff` `Continuous.continuousAt` `continuous_inr` `ContDiffWithinAt.congr_of_eventuallyEq` `contDiffWithinAt_id` `ModelWithCorners.image_eq` `OpenPartialHomeomorph.extend_image_target_mem_nhds` `mem_chart_source` `Filter.mp_mem` `Filter.univ_mem'` `nonempty_of_chartedSpace` `Topology.IsOpenEmbedding.inr` `ChartedSpace.sum_chartAt_inr` `OpenPartialHomeomorph.lift_openEmbedding.congr_simp` `Function.Injective.extend_apply` `Sum.inr_injective` `OpenPartialHomeomorph.right_inv` `ModelWithCorners.right_inv` `ModelWithCorners.left_inv` `OpenPartialHomeomorph.left_inv`
`prodMap` 📖	mathematical	`ContMDiff`	`Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	—	`ContMDiffAt.prodMap'`
`prodMk` 📖	mathematical	`ContMDiff`	`Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	—	`ContMDiffAt.prodMk`
`prodMk_space` 📖	mathematical	`ContMDiff` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf`	`Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `instTopologicalSpaceProd`	—	`ContMDiffAt.prodMk_space`
`snd` 📖	—	`ContMDiff` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	—	—	`comp` `contMDiff_snd`
`sumElim` 📖	mathematical	`ContMDiff`	`instTopologicalSpaceSum` `ChartedSpace.sum`	—	`contMDiffAt_iff` `Continuous.continuousAt` `Continuous.sumElim` `continuous` `sum_chartAt_inl_apply` `ContDiffWithinAt.congr_of_eventuallyEq` `nonempty_of_chartedSpace` `Topology.IsOpenEmbedding.inl` `ChartedSpace.sum_chartAt_inl` `Filter.univ_mem'` `sum_chartAt_inr_apply` `Topology.IsOpenEmbedding.inr` `ChartedSpace.sum_chartAt_inr`
`sumMap` 📖	mathematical	`ContMDiff`	`instTopologicalSpaceSum` `ChartedSpace.sum`	—	`sumElim` `comp` `inl` `inr`
`swap` 📖	mathematical	—	`ContMDiff` `instTopologicalSpaceSum` `ChartedSpace.sum`	—	`sumElim` `inr` `inl`

ContMDiffAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`along_fst` 📖	—	`ContMDiffAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	—	—	`curry_left`
`along_snd` 📖	—	`ContMDiffAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	—	—	`curry_right`
`comp₂` 📖	—	`ContMDiffAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	—	—	`comp` `prodMk`
`comp₂_of_eq` 📖	—	`ContMDiffAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	—	—	`comp₂`
`curry_left` 📖	—	`ContMDiffAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	—	—	`comp₂` `contMDiffAt_id` `contMDiffAt_const`
`curry_right` 📖	—	`ContMDiffAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	—	—	`comp₂` `contMDiffAt_const` `contMDiffAt_id`
`fst` 📖	—	`ContMDiffAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	—	—	`comp` `contMDiffAt_fst`
`prodMap` 📖	mathematical	`ContMDiffAt`	`Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	—	`ContMDiffWithinAt.prodMap`
`prodMap'` 📖	mathematical	`ContMDiffAt`	`Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	—	`prodMap`
`prodMk` 📖	mathematical	`ContMDiffAt`	`Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	—	`ContMDiffWithinAt.prodMk`
`prodMk_space` 📖	mathematical	`ContMDiffAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf`	`Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `instTopologicalSpaceProd`	—	`ContMDiffWithinAt.prodMk_space`
`snd` 📖	—	`ContMDiffAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	—	—	`comp` `contMDiffAt_snd`

ContMDiffOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`along_fst` 📖	mathematical	`ContMDiffOn` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	`setOf` `Set` `Set.instMembership`	—	`curry_left`
`along_snd` 📖	mathematical	`ContMDiffOn` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	`setOf` `Set` `Set.instMembership`	—	`curry_right`
`curry_left` 📖	mathematical	`ContMDiffOn` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	`setOf` `Set` `Set.instMembership`	—	`ContMDiffWithinAt.along_fst`
`curry_right` 📖	mathematical	`ContMDiffOn` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	`setOf` `Set` `Set.instMembership`	—	`ContMDiffWithinAt.along_snd`
`prodMap` 📖	mathematical	`ContMDiffOn`	`Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace` `SProd.sprod` `Set` `Set.instSProd`	—	`prodMk` `comp` `contMDiffOn_fst` `Set.mapsTo_fst_prod` `contMDiffOn_snd` `Set.mapsTo_snd_prod`
`prodMk` 📖	mathematical	`ContMDiffOn`	`Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	—	`ContMDiffWithinAt.prodMk`
`prodMk_space` 📖	mathematical	`ContMDiffOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf`	`Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `instTopologicalSpaceProd`	—	`ContMDiffWithinAt.prodMk_space`

ContMDiffWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`along_fst` 📖	mathematical	`ContMDiffWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	`setOf` `Set` `Set.instMembership`	—	`curry_left`
`along_snd` 📖	mathematical	`ContMDiffWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	`setOf` `Set` `Set.instMembership`	—	`curry_right`
`comp₂` 📖	—	`ContMDiffWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace` `Set.MapsTo`	—	—	`comp` `prodMk`
`comp₂_of_eq` 📖	—	`ContMDiffWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace` `Set.MapsTo`	—	—	`comp₂`
`curry_left` 📖	mathematical	`ContMDiffWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	`setOf` `Set` `Set.instMembership`	—	`comp₂` `contMDiffWithinAt_id` `contMDiffWithinAt_const`
`curry_right` 📖	mathematical	`ContMDiffWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	`setOf` `Set` `Set.instMembership`	—	`comp₂` `contMDiffWithinAt_const` `contMDiffWithinAt_id`
`fst` 📖	—	`ContMDiffWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	—	—	`comp` `contMDiffWithinAt_fst` `Set.mapsTo_image`
`prodMap` 📖	mathematical	`ContMDiffWithinAt`	`Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace` `SProd.sprod` `Set` `Set.instSProd`	—	`prodMap'`
`prodMap'` 📖	mathematical	`ContMDiffWithinAt`	`Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace` `SProd.sprod` `Set` `Set.instSProd`	—	`prodMk` `comp` `contMDiffWithinAt_fst` `Set.mapsTo_fst_prod` `contMDiffWithinAt_snd` `Set.mapsTo_snd_prod`
`prodMk` 📖	mathematical	`ContMDiffWithinAt`	`Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	—	`contMDiffWithinAt_iff` `ContinuousWithinAt.prodMk` `ContDiffWithinAt.prodMk`
`prodMk_space` 📖	mathematical	`ContMDiffWithinAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf`	`Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `instTopologicalSpaceProd`	—	`contMDiffWithinAt_iff` `ContinuousWithinAt.prodMk` `ContDiffWithinAt.prodMk`
`snd` 📖	—	`ContMDiffWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	—	—	`comp` `contMDiffWithinAt_snd` `Set.mapsTo_image`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`contMDiffAt_fst` 📖	mathematical	—	`ContMDiffAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	—	`contMDiffWithinAt_fst`
`contMDiffAt_pi_space` 📖	mathematical	—	`ContMDiffAt` `Pi.normedAddCommGroup` `Pi.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `modelWithCornersSelf` `Pi.topologicalSpace` `chartedSpaceSelf`	—	`contMDiffWithinAt_pi_space`
`contMDiffAt_prod_iff` 📖	mathematical	—	`ContMDiffAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	—	`contMDiffWithinAt_prod_iff`
`contMDiffAt_prod_module_iff` 📖	mathematical	—	`ContMDiffAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `modelWithCornersSelf` `instTopologicalSpaceProd` `chartedSpaceSelf`	—	`modelWithCornersSelf_prod` `chartedSpaceSelf_prod` `contMDiffAt_prod_iff`
`contMDiffAt_snd` 📖	mathematical	—	`ContMDiffAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	—	`contMDiffWithinAt_snd`
`contMDiffOn_fst` 📖	mathematical	—	`ContMDiffOn` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	—	`contMDiffWithinAt_fst`
`contMDiffOn_pi_space` 📖	mathematical	—	`ContMDiffOn` `Pi.normedAddCommGroup` `Pi.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `modelWithCornersSelf` `Pi.topologicalSpace` `chartedSpaceSelf`	—	`contMDiffWithinAt_pi_space`
`contMDiffOn_prod_iff` 📖	mathematical	—	`ContMDiffOn` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	—	`contMDiffWithinAt_prod_iff`
`contMDiffOn_prod_module_iff` 📖	mathematical	—	`ContMDiffOn` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `modelWithCornersSelf` `instTopologicalSpaceProd` `chartedSpaceSelf`	—	`modelWithCornersSelf_prod` `chartedSpaceSelf_prod` `contMDiffOn_prod_iff`
`contMDiffOn_snd` 📖	mathematical	—	`ContMDiffOn` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	—	`contMDiffWithinAt_snd`
`contMDiffWithinAt_fst` 📖	mathematical	—	`ContMDiffWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	—	`contMDiffWithinAt_iff'` `continuousWithinAt_fst` `ContDiffWithinAt.congr` `contDiffWithinAt_fst` `PartialEquiv.right_inv` `PartialEquiv.map_source` `mem_extChartAt_source`
`contMDiffWithinAt_pi_space` 📖	mathematical	—	`ContMDiffWithinAt` `Pi.normedAddCommGroup` `Pi.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `modelWithCornersSelf` `Pi.topologicalSpace` `chartedSpaceSelf`	—	`extChartAt_model_space_eq_id`
`contMDiffWithinAt_prod_iff` 📖	mathematical	—	`ContMDiffWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	—	`ContMDiffWithinAt.fst` `ContMDiffWithinAt.snd` `ContMDiffWithinAt.prodMk`
`contMDiffWithinAt_prod_module_iff` 📖	mathematical	—	`ContMDiffWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `modelWithCornersSelf` `instTopologicalSpaceProd` `chartedSpaceSelf`	—	`modelWithCornersSelf_prod` `chartedSpaceSelf_prod` `contMDiffWithinAt_prod_iff`
`contMDiffWithinAt_snd` 📖	mathematical	—	`ContMDiffWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	—	`contMDiffWithinAt_iff'` `continuousWithinAt_snd` `ContDiffWithinAt.congr` `contDiffWithinAt_snd` `PartialEquiv.right_inv` `PartialEquiv.map_source` `mem_extChartAt_source`
`contMDiff_fst` 📖	mathematical	—	`ContMDiff` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	—	`contMDiffAt_fst`
`contMDiff_of_contMDiff_inl` 📖	—	`ContMDiff` `instTopologicalSpaceSum` `ChartedSpace.sum`	—	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `Nontrivial.to_nonempty` `contMDiffOn_univ` `ContMDiffOn.comp` `ContMDiff.contMDiffOn` `ContMDiff.sumElim` `contMDiff_id` `contMDiff_const` `Set.mem_preimage`
`contMDiff_of_contMDiff_inr` 📖	—	`ContMDiff` `instTopologicalSpaceSum` `ChartedSpace.sum`	—	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `Nontrivial.to_nonempty` `contMDiffOn_univ` `ContMDiffOn.comp` `ContMDiff.contMDiffOn` `ContMDiff.sumElim` `contMDiff_const` `contMDiff_id` `Set.mem_preimage`
`contMDiff_pi_space` 📖	mathematical	—	`ContMDiff` `Pi.normedAddCommGroup` `Pi.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `modelWithCornersSelf` `Pi.topologicalSpace` `chartedSpaceSelf`	—	`contMDiffAt_pi_space`
`contMDiff_prod_assoc` 📖	mathematical	—	`ContMDiff` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	—	`ContMDiff.prodMk` `ContMDiff.fst` `contMDiff_fst` `ContMDiff.snd` `contMDiff_snd`
`contMDiff_prod_iff` 📖	mathematical	—	`ContMDiff` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	—	`ContMDiff.fst` `ContMDiff.snd` `ContMDiff.prodMk`
`contMDiff_prod_module_iff` 📖	mathematical	—	`ContMDiff` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `modelWithCornersSelf` `instTopologicalSpaceProd` `chartedSpaceSelf`	—	`modelWithCornersSelf_prod` `chartedSpaceSelf_prod` `contMDiff_prod_iff`
`contMDiff_snd` 📖	mathematical	—	`ContMDiff` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	—	`contMDiffAt_snd`
`contMDiff_sum_map` 📖	mathematical	—	`ContMDiff` `instTopologicalSpaceSum` `ChartedSpace.sum`	—	`contMDiff_of_contMDiff_inl` `ContMDiff.comp` `ContMDiff.inl` `contMDiff_of_contMDiff_inr` `ContMDiff.inr` `ContMDiff.sumMap`
`extChartAt_inl_apply` 📖	mathematical	—	`PartialEquiv.toFun` `extChartAt` `instTopologicalSpaceSum` `ChartedSpace.sum`	—	`sum_chartAt_inl_apply`
`extChartAt_inr_apply` 📖	mathematical	—	`PartialEquiv.toFun` `extChartAt` `instTopologicalSpaceSum` `ChartedSpace.sum`	—	`sum_chartAt_inr_apply`

---

← Back to Index