Library ▹ Essentials ▹ Sets
Definition 1.1.1.  We define:
∅ := {}
Remarks.

This defines the empty set as an enumeration with no elements. Note that sets are a built-in concept in the HLM logic.

References.
  • https://en.wikipedia.org/wiki/Empty_set
  • https://mathworld.wolfram.com/EmptySet.html
  • https://proofwiki.org/wiki/Definition:Empty_Set
  • https://ncatlab.org/nlab/show/empty+set
  • http://metamath.tirix.org/df-nul.html
  • https://leanprover-community.github.io/mathlib_docs/data/set/basic.html#set.empty_def
[View Source]