Commit 2024-09-05 23:22 ad40d932

View on Github →

chore(TopologicalSpace.Opens): introduce Opens.inclusion (#16513) Currently we use Set.inclusion to construct functions between Opens. This is a form of defeq abuse which is exposed by leanprover/lean4#5020. In this PR, we introduce Opens.inclusion and replace uses of Set.inclusion with it to avoid passing through a coercion to Set. Since there is a version, not analogous to Set.inclusion, squatting on this name we rename it to Opens.inclusion'.

Estimated changes

Modified Mathlib/AlgebraicGeometry/AffineScheme.lean

Modified Mathlib/AlgebraicGeometry/OpenImmersion.lean

Modified Mathlib/AlgebraicGeometry/Restrict.lean

Modified Mathlib/Geometry/Manifold/ChartedSpace.lean

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

Modified Mathlib/Geometry/Manifold/LocalInvariantProperties.lean

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

Modified Mathlib/Geometry/Manifold/Sheaf/LocallyRingedSpace.lean

Modified Mathlib/Geometry/RingedSpace/PresheafedSpace.lean

Modified Mathlib/Topology/Category/TopCat/OpenNhds.lean

modified theorem TopologicalSpace.OpenNhds.openEmbedding

Modified Mathlib/Topology/Category/TopCat/Opens.lean

added theorem TopologicalSpace.Opens.coe_inclusion'

deleted theorem TopologicalSpace.Opens.coe_inclusion

added def TopologicalSpace.Opens.inclusion'

added theorem TopologicalSpace.Opens.inclusion'_map_eq_top

added theorem TopologicalSpace.Opens.inclusion'_top_functor

deleted def TopologicalSpace.Opens.inclusion

deleted theorem TopologicalSpace.Opens.inclusion_map_eq_top

deleted theorem TopologicalSpace.Opens.inclusion_top_functor

modified theorem TopologicalSpace.Opens.openEmbedding

added theorem TopologicalSpace.Opens.set_range_forget_map_inclusion'

deleted theorem TopologicalSpace.Opens.set_range_forget_map_inclusion

Modified Mathlib/Topology/Gluing.lean

Modified Mathlib/Topology/Sets/Opens.lean