Definition 1.1.4.  Let S be a set. We define:
S is finite  :⇔  |S| is finite  ⇔  ∃ k ∈ , f:S ↔ ℕ<k  ⇔  ∃ l ∈ , g: ℕ<l ↔ S  ⇔  ∃ m ∈ , h:S → ℕ<m : h is injective  ⇔  ∃ n ∈ , i:S → ℕn : i is injective
S is infinite  :⇔  S is not finite
Equivalence.
Remarks.

This definition uses functions as well as the natural and cardinal numbers, all of which are defined in later sections (see $../Functions/Functions, $../Numbers/Natural/"Natural numbers", $../Numbers/Cardinal/"Cardinal numbers"). That is not a problem as long as no circularities exist. In other words, definitions and theorems are ordered by topic instead of by dependency.

References.