Commit 2024-10-08 21:50 2d2e3987

View on Github →

feat(Logic/Function): define Pi.map (#17482) Also use it instead of dcomp or an inline lambda here and there.

Estimated changes

Modified Mathlib/Algebra/Group/Pi/Basic.lean

deleted theorem Function.bijective_pi_map

deleted theorem Function.injective_pi_map

deleted theorem Function.surjective_pi_map

Modified Mathlib/CategoryTheory/MorphismProperty/Limits.lean

Modified Mathlib/CategoryTheory/Triangulated/Basic.lean

Modified Mathlib/CategoryTheory/Triangulated/Pretriangulated.lean

Modified Mathlib/Data/Set/Prod.lean

deleted theorem Set.dcomp_image_pi

deleted theorem Set.dcomp_image_univ_pi

added theorem Set.piMap_image_pi

added theorem Set.piMap_image_univ_pi

deleted theorem Set.range_dcomp

added theorem Set.range_piMap

Modified Mathlib/Logic/Equiv/Basic.lean

Modified Mathlib/Logic/Equiv/PartialEquiv.lean

Modified Mathlib/Logic/Function/Basic.lean

added theorem Function.Bijective.piMap

modified theorem Function.Injective.comp_left

added theorem Function.Injective.piMap

added theorem Function.Surjective.piMap

Modified Mathlib/Logic/Function/Defs.lean

added theorem Pi.map_apply

Modified Mathlib/Topology/MetricSpace/IsometricSMul.lean

Modified Mathlib/Topology/MetricSpace/Isometry.lean

deleted theorem isometry_dcomp