Commit 2024-09-19 11:58 b3592187

View on Github →

feat(Topology): the partition of a space into fibers of a function (#15527)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Logic/Function/FiberPartition.lean

added theorem Function.Fiber.eq_fiber_image

added theorem Function.Fiber.fiber_nonempty

added theorem Function.Fiber.image_eq_image_mk

added theorem Function.Fiber.map_eq_image

added theorem Function.Fiber.map_preimage_eq_image

added theorem Function.Fiber.map_preimage_eq_image_map

added theorem Function.Fiber.mem_iff_eq_image

added def Function.Fiber.mk

added def Function.Fiber.mkSelf

added theorem Function.Fiber.mk_image

added def Function.Fiber

Created Mathlib/Topology/FiberPartition.lean

added def TopologicalSpace.Fiber.sigmaIncl

added def TopologicalSpace.Fiber.sigmaInclIncl

added def TopologicalSpace.Fiber.sigmaIsoHom

added theorem TopologicalSpace.Fiber.sigmaIsoHom_inj

added theorem TopologicalSpace.Fiber.sigmaIsoHom_surj