Slate - empty

Definition 1.1.3. Let S be a set. We define:

S is empty :⇔ S = ∅ ⇔ S ⊆ ∅ ⇔ ∄ x ∈ S ⇔ |S| = 0 ⇔ |S| ≤ 0

S is nonempty :⇔ S is not empty

Equivalence.

Assume S = ∅. Then ∄ x ∈ S:
Let x ∈ S.
⇒^S = ∅ x ∈ ∅⇒^def ↯
Assume ∄ x ∈ S. Then S ⊆ ∅:
Let a ∈ S. Then a ∈ ∅:
We have ∃ x ∈ S: ↯
Take x := a.
Assume S ⊆ ∅. Then S = ∅:
- Trivial.
- By 1.1.2.
Assume S = ∅. Then |S| = 0:
We have |S| = |∅| = |ℕ_<0| = 0.
Assume |S| = 0. Then |S| ≤ 0:
We show that 0 ≤ 0:
1.8.2.10 ⇒ ≤ is a partial order ⇒^def ≤ is reflexive ⇒^def ∀ κ ∈ Crd : κ ≤ κ ⇒^{0 ∈ Crd} 0 ≤ 0
Assume |S| ≤ 0. Then ∄ x ∈ S:
|S| ≤ 0 ⇒^def ∃ φ : |S| → 0 : φ is injective
Let x ∈ S.
We have φ(x) ∈ ℕ_<0 ⇒^def φ(x) < 0 ⇒^def ↯.

Remarks.

In HLM, multiple alternative definitions can be given for an operator or predicate, if they can be shown to be equal/equivalent. In proofs, the most convenient alternative can be selected at will, which reduces the number of necessary steps. Sometimes, it also makes sense to prove a property according to one alternative and then use it according to another.

References.

https://leanprover-community.github.io/mathlib_docs/data/set/basic.html#set.nonempty