Commit 2024-11-18 06:07 d2568da6

View on Github →

feat(Topology/Sheaves/Stalks): Generalize to stalkPushforward_iso_of_inducing (#18268) port of https://github.com/leanprover-community/mathlib3/pull/17539

Estimated changes

Modified Mathlib/Geometry/RingedSpace/OpenImmersion.lean

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

added def Topology.IsInducing.adjunctionNhds

added def Topology.IsInducing.functorNhds

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

added def Topology.IsInducing.adjunction

added def Topology.IsInducing.functor

added def Topology.IsInducing.functorObj

added theorem Topology.IsInducing.le_functorObj_iff

added theorem Topology.IsInducing.map_functorObj

added theorem Topology.IsInducing.mem_functorObj_iff

added def Topology.IsInducing.opensGI

Modified Mathlib/Topology/Sheaves/Stalks.lean

added theorem TopCat.Presheaf.stalkPushforward.stalkPushforward_iso_of_isInducing

deleted theorem TopCat.Presheaf.stalkPushforward.stalkPushforward_iso_of_isOpenEmbedding