mathlib Merge 3 files about basic properties of relations

Merge 3 files about basic properties of relations

Open urkud opened this issue 6 years ago • 3 comments

We have at least 3 files with basic facts about relations.

data/rel defines https://github.com/leanprover-community/mathlib/blob/708faa9f3dba94a57e26ebd27a87cc6cd77a4d06/src/data/rel.lean#L12 then defines (pre)image, (co)domain, composition etc.
logic/relation works with α → β → Prop without introducing a type name. https://github.com/leanprover-community/mathlib/blob/708faa9f3dba94a57e26ebd27a87cc6cd77a4d06/src/logic/relation.lean#L11-L16
topology/uniform_space/basic deals with set (α × β) without introducing a type name. https://github.com/leanprover-community/mathlib/blob/708faa9f3dba94a57e26ebd27a87cc6cd77a4d06/src/topology/uniform_space/basic.lean#L39-L47

See also https://github.com/leanprover-community/mathlib/blob/708faa9f3dba94a57e26ebd27a87cc6cd77a4d06/src/logic/relator.lean#L26-L29

Sep 28 '19 16:09 urkud