Commit 2022-11-17 13:19 e872bdbc

View on Github →

feat: port logic.pairwise (#622) mathlib3 sha: 70fd9563a21e7b963887c9360bd29b2393e6225a Added an extra align because mathport got it wrong in the ported file.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Logic/Function/Basic.lean

Created Mathlib/Logic/Pairwise.lean

added theorem Function.injective_iff_pairwise_ne

added theorem Pairwise.mono

added theorem Pairwise.set_pairwise

added def Pairwise

added theorem Reflexive.set_pairwise_iff

added theorem Set.Pairwise.imp

added theorem Set.Pairwise.imp_on

added theorem Set.Pairwise.on_injective

added theorem Set.pairwise_of_forall