mathlib
909cae04 - feat(logic/basic): given two different elements, one of the two is different from a third (#16023)

Commit

3 years ago

feat(logic/basic): given two different elements, one of the two is different from a third (#16023) This lemma is extracted from #15984, as suggested by the code-review.

Author

adomani

Parents

33261fbe

mathlib 909cae04 - feat(logic/basic): given two different elements, one of the two is different from a third (#16023)

mathlib
909cae04 - feat(logic/basic): given two different elements, one of the two is different from a third (#16023)