Library ▹ Essentials ▹ Relations
Definition 1.4.9.  Let S be a set, ⪯ be a relation on S. We define:
⪯ is reflexive  :⇔  ∀ s ∈ S : s ⪯ s
References.
  • https://en.wikipedia.org/wiki/Reflexive_relation
  • https://mathworld.wolfram.com/Reflexive.html
  • https://proofwiki.org/wiki/Definition:Reflexive_Relation
  • https://ncatlab.org/nlab/show/reflexive+relation
  • https://coq.inria.fr/library/Coq.Sets.Relations_1.html#Reflexive
  • https://leanprover-community.github.io/mathlib_docs/init/logic.html#reflexive
[View Source]