Commit 2025-12-10 04:42 64832b9b

View on Github →

feat: product of immersions is an immersion (#28853)

Estimated changes

Modified Mathlib/Data/Set/Prod.lean

added theorem Set.EqOn.left_of_eqOn_prodMap

added theorem Set.EqOn.prodMap

added theorem Set.EqOn.right_of_eqOn_prodMap

added theorem Set.eqOn_prodMap_iff

added theorem Set.eqOn_prod_iff

Modified Mathlib/Geometry/Manifold/Immersion.lean

added theorem Manifold.IsImmersion.prodMap

added theorem Manifold.IsImmersionAt.prodMap

added theorem Manifold.IsImmersionAtOfComplement.prodMap

added theorem Manifold.IsImmersionOfComplement.prodMap

Modified Mathlib/Geometry/Manifold/IsManifold/Basic.lean

added theorem IsManifold.mem_maximalAtlas_iff

added theorem IsManifold.mem_maximalAtlas_prod

Modified Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean

added theorem OpenPartialHomeomorph.extend_prod

Modified Mathlib/Geometry/Manifold/LocalSourceTargetProperty.lean

modified theorem Manifold.LiftSourceTargetPropertyAt.codChart_mem_maximalAtlas

modified theorem Manifold.LiftSourceTargetPropertyAt.domChart_mem_maximalAtlas

modified theorem Manifold.LiftSourceTargetPropertyAt.mem_codChart_source

modified theorem Manifold.LiftSourceTargetPropertyAt.mem_domChart_source

added theorem Manifold.LiftSourceTargetPropertyAt.prodMap

modified theorem Manifold.LiftSourceTargetPropertyAt.property

Modified Mathlib/Topology/OpenPartialHomeomorph/Constructions.lean

added theorem OpenPartialHomeomorph.prod_symm_trans_prod