Commit 2026-03-17 12:17 d81f18c5

View on Github →

feat: more API for Function.IsPartialInv (#36471) This also renames some lemmas to enable dot notation.

Estimated changes

Modified Mathlib/Data/Set/Finite/Basic.lean

Modified Mathlib/Logic/Encodable/Basic.lean

added theorem Encodable.decode₂_isPartialInv

deleted theorem Encodable.decode₂_is_partial_inv

Modified Mathlib/Logic/Function/Basic.lean

added theorem Function.Injective.isPartialInv

added theorem Function.IsPartialInv.comp

added theorem Function.IsPartialInv.eq

added theorem Function.IsPartialInv.get_eq

added theorem Function.IsPartialInv.injective

added theorem Function.IsPartialInv.surjective_getD

deleted theorem Function.injective_of_isPartialInv

deleted theorem Function.isPartialInv_left

deleted theorem Function.partialInv_of_injective